begin
This theory continues the series on general topology and covers the definition and basic properties of continuous functions. We also introduce the notion of homeomorphism an prove the pasting lemma.
Continuous functions.
In this section we define continuous functions and prove that certain conditions are equivalent to a function being continuous.
In standard math we say that a function is continuous with respect to two topologies \(\tau_1 ,\tau_2 \) if the inverse image of sets from topology \(\tau_2\) are in \(\tau_1\). Here we define a predicate that is supposed to reflect that definition, with a difference that we don't require in the definition that \(\tau_1 ,\tau_2 \) are topologies. This means for example that when we define measurable functions, the definition will be the same. The notation \( f^{-1}(A) \) means the inverse image of (a set) \(A\) with respect to (a function) \(f\).
definition
\( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
The space of continuous functions mapping \(X=\bigcup \tau_1\) to \(Y=\bigcup \tau_2\) will be denoted \( \text{Cont}(\tau _1,\tau _2) \).
definition
\( \text{Cont}(\tau _1,\tau _2) \equiv \{f\in (\bigcup \tau _1)\rightarrow (\bigcup \tau _2).\ \text{IsContinuous}(\tau _1,\tau _2,f)\} \)
A trivial example of a continuous function - identity is continuous.
lemma id_cont:
shows \( \text{IsContinuous}(\tau ,\tau ,id(\bigcup \tau )) \)proof{
}
fix \( U \)
assume \( U\in \tau \)
then have \( id(\bigcup \tau )^{-1}(U) = U \) using vimage_id_same
with \( U\in \tau \) have \( id(\bigcup \tau )^{-1}(U) \in \tau \)
then show \( \text{IsContinuous}(\tau ,\tau ,id(\bigcup \tau )) \) unfolding IsContinuous_def
qed
Identity is in the space of continuous functions from \(\bigcup \tau\) to itself.
lemma id_cont_sp:
shows \( \{\langle x,x\rangle .\ x\in \bigcup \tau \} \in \text{Cont}(\tau ,\tau ) \)proof have \( id(\bigcup \tau ) : \bigcup \tau \rightarrow \bigcup \tau \) and \( \text{IsContinuous}(\tau ,\tau ,id(\bigcup \tau )) \) using id_type, id_cont
moreover
qed
have \( id(\bigcup \tau ) = \{\langle x,x\rangle .\ x\in \bigcup \tau \} \)
ultimately show \( thesis \) unfolding Cont_def
A constant function is continuous.
lemma const_cont:
assumes \( T \text{ is a topology } \)
shows \( \text{IsContinuous}(T,\tau , \text{ConstantFunction}(\bigcup T,c)) \)proof let \( C = \text{ConstantFunction}(\bigcup T,c) \)
{
fix \( U \)
assume \( U\in \tau \)
have \( C^{-1}(U) \in T \)proof
{
}
assume \( c\in U \)
with assms have \( C^{-1}(U) \in T \) using carr_open, const_vimage_domain
moreover {
}
ultimately show \( C^{-1}(U) \in T \)
qed
assume \( c\notin U \)
with assms have \( C^{-1}(U) \in T \) using empty_open, const_vimage_empty
then show \( thesis \) unfolding IsContinuous_def
qed
If \(c\in Y = \bigcup S\), then the constant function defined on \(X=\bigcup T \) that is equal to \(c\) is in the the space of continuous functions from \(X\) to \(Y\).
lemma const_cont_sp:
assumes \( T \text{ is a topology } \), \( c\in \bigcup S \)
shows \( \{\langle x,c\rangle .\ x\in \bigcup T\} \in \text{Cont}(T,S) \) using assms, ZF_fun_from_total, const_fun_def_alt, const_cont unfolding Cont_defWe will work with a pair of topological spaces. The following locale sets up our context that consists of two topologies \(\tau_1,\tau_2\) and a continuous function \(f: X_1 \rightarrow X_2\), where \(X_i\) is defined as \(\bigcup\tau_i\) for \(i=1,2\). We also define notation \( cl_1(A) \) and \( cl_2(A) \) for closure of a set \(A\) in topologies \(\tau_1\) and \(\tau_2\), respectively.
locale two_top_spaces0
assumes tau1_is_top: \( \tau _1 \text{ is a topology } \)
assumes tau2_is_top: \( \tau _2 \text{ is a topology } \)
defines \( X_1 \equiv \bigcup \tau _1 \)
defines \( X_2 \equiv \bigcup \tau _2 \)
assumes fmapAssum: \( f: X_1 \rightarrow X_2 \)
defines \( g \text{ is continuous } \equiv \text{IsContinuous}(\tau _1,\tau _2,g) \)
defines \( cl_1(A) \equiv \text{Closure}(A,\tau _1) \)
defines \( cl_2(A) \equiv \text{Closure}(A,\tau _2) \)
First we show that theorems proven in locale topology0 are valid when applied to topologies \(\tau_1\) and \(\tau_2\).
lemma (in two_top_spaces0) topol_cntxs_valid:
shows \( topology0(\tau _1) \) and \( topology0(\tau _2) \) using tau1_is_top, tau2_is_top, topology0_defFor continuous functions the inverse image of a closed set is closed.
lemma (in two_top_spaces0) TopZF_2_1_L1:
assumes A1: \( f \text{ is continuous } \) and A2: \( D \text{ is closed in } \tau _2 \)
shows \( f^{-1}(D) \text{ is closed in } \tau _1 \)proof from fmapAssum have \( f^{-1}(D) \subseteq X_1 \) using func1_1_L3
moreover
from fmapAssum have \( f^{-1}(X_2 - D) = X_1 - f^{-1}(D) \) using Pi_iff, function_vimage_Diff, func1_1_L4
ultimately have \( X_1 - f^{-1}(X_2 - D) = f^{-1}(D) \)
moreover
qed
from A1, A2 have \( (X_1 - f^{-1}(X_2 - D)) \text{ is closed in } \tau _1 \) using IsClosed_def, IsContinuous_def, topol_cntxs_valid, Top_3_L9
ultimately show \( f^{-1}(D) \text{ is closed in } \tau _1 \)
If the inverse image of every closed set is closed, then the image of a closure is contained in the closure of the image.
lemma (in two_top_spaces0) Top_ZF_2_1_L2:
assumes A1: \( \forall D.\ ((D \text{ is closed in } \tau _2) \longrightarrow f^{-1}(D) \text{ is closed in } \tau _1) \) and A2: \( A \subseteq X_1 \)
shows \( f(cl_1(A)) \subseteq cl_2(f(A)) \)proof from fmapAssum have \( f(A) \subseteq cl_2(f(A)) \) using func1_1_L6, topol_cntxs_valid, cl_contains_set
with fmapAssum have \( f^{-1}(f(A)) \subseteq f^{-1}(cl_2(f(A))) \)
moreover
from fmapAssum, A2 have \( A \subseteq f^{-1}(f(A)) \) using func1_1_L9
ultimately have \( A \subseteq f^{-1}(cl_2(f(A))) \)
with fmapAssum, A1 have \( f(cl_1(A)) \subseteq f(f^{-1}(cl_2(f(A)))) \) using func1_1_L6, func1_1_L8, IsClosed_def, topol_cntxs_valid, cl_is_closed, Top_3_L13
moreover
qed
from fmapAssum have \( f(f^{-1}(cl_2(f(A)))) \subseteq cl_2(f(A)) \) using fun_is_function, function_image_vimage
ultimately show \( f(cl_1(A)) \subseteq cl_2(f(A)) \)
If \(f\left( \overline{A}\right)\subseteq \overline{f(A)}\) (the image of the closure is contained in the closure of the image), then \(\overline{f^{-1}(B)}\subseteq f^{-1}\left( \overline{B} \right)\) (the inverse image of the closure contains the closure of the inverse image).
lemma (in two_top_spaces0) Top_ZF_2_1_L3:
assumes A1: \( \forall A.\ ( A \subseteq X_1 \longrightarrow f(cl_1(A)) \subseteq cl_2(f(A))) \)
shows \( \forall B.\ ( B \subseteq X_2 \longrightarrow cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) ) \)proof{
}
fix \( B \)
assume \( B \subseteq X_2 \)
from fmapAssum, A1 have \( f(cl_1(f^{-1}(B))) \subseteq cl_2(f(f^{-1}(B))) \) using func1_1_L3
moreover
from fmapAssum, \( B \subseteq X_2 \) have \( cl_2(f(f^{-1}(B))) \subseteq cl_2(B) \) using fun_is_function, function_image_vimage, func1_1_L6, topol_cntxs_valid, top_closure_mono
ultimately have \( f^{-1}(f(cl_1(f^{-1}(B)))) \subseteq f^{-1}(cl_2(B)) \) using fmapAssum, fun_is_function
moreover
from fmapAssum, \( B \subseteq X_2 \) have \( cl_1(f^{-1}(B)) \subseteq f^{-1}(f(cl_1(f^{-1}(B)))) \) using func1_1_L3, func1_1_L9, IsClosed_def, topol_cntxs_valid, cl_is_closed
ultimately have \( cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) \)
then show \( thesis \)
qed
If \(\overline{f^{-1}(B)}\subseteq f^{-1}\left( \overline{B} \right)\) (the inverse image of a closure contains the closure of the inverse image), then the function is continuous. This lemma closes a series of implications in lemmas Top_ZF_2_1_L1, Top_ZF_2_1_L2 and Top_ZF_2_1_L3 showing equivalence of four definitions of continuity.
lemma (in two_top_spaces0) Top_ZF_2_1_L4:
assumes A1: \( \forall B.\ ( B \subseteq X_2 \longrightarrow cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) ) \)
shows \( f \text{ is continuous } \)proof{
}
fix \( U \)
assume \( U \in \tau _2 \)
then have \( (X_2 - U) \text{ is closed in } \tau _2 \) using topol_cntxs_valid, Top_3_L9
moreover
have \( X_2 - U \subseteq \bigcup \tau _2 \)
ultimately have \( cl_2(X_2 - U) = X_2 - U \) using topol_cntxs_valid, Top_3_L8
moreover
from A1 have \( cl_1(f^{-1}(X_2 - U)) \subseteq f^{-1}(cl_2(X_2 - U)) \)
ultimately have \( cl_1(f^{-1}(X_2 - U)) \subseteq f^{-1}(X_2 - U) \)
moreover
from fmapAssum have \( f^{-1}(X_2 - U) \subseteq cl_1(f^{-1}(X_2 - U)) \) using func1_1_L3, topol_cntxs_valid, cl_contains_set
ultimately have \( f^{-1}(X_2 - U) \text{ is closed in } \tau _1 \) using fmapAssum, func1_1_L3, topol_cntxs_valid, Top_3_L8
with fmapAssum have \( f^{-1}(U) \in \tau _1 \) using fun_is_function, function_vimage_Diff, func1_1_L4, func1_1_L3, IsClosed_def, double_complement
then have \( \forall U\in \tau _2.\ f^{-1}(U) \in \tau _1 \)
then show \( thesis \) using IsContinuous_def
qed
For continuous functions the closure of the inverse image is contained in the inverse image of the closure. This is a shortcut through a series of implications provided by TopZF_2_1_L1, Top_ZF_2_1_L2 and Top_ZF_2_1_L3.
corollary (in two_top_spaces0) im_cl_in_cl_im:
assumes \( f \text{ is continuous } \) and \( B \subseteq X_2 \)
shows \( cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) \) using assms, TopZF_2_1_L1, Top_ZF_2_1_L2, Top_ZF_2_1_L3Another condition for continuity: it is sufficient to check if the inverse image of every set in a base is open.
lemma (in two_top_spaces0) Top_ZF_2_1_L5:
assumes A1: \( B \text{ is a base for } \tau _2 \) and A2: \( \forall U\in B.\ f^{-1}(U) \in \tau _1 \)
shows \( f \text{ is continuous } \)proof{
}
fix \( V \)
assume A3: \( V \in \tau _2 \)
with A1 obtain \( A \) where \( A \subseteq B \), \( V = \bigcup A \) using IsAbaseFor_def
with A2 have \( \{f^{-1}(U).\ U\in A\} \subseteq \tau _1 \)
with tau1_is_top have \( \bigcup \{f^{-1}(U).\ U\in A\} \in \tau _1 \) using IsATopology_def
moreover
from \( A \subseteq B \), \( V = \bigcup A \) have \( f^{-1}(V) = \bigcup \{f^{-1}(U).\ U\in A\} \)
ultimately have \( f^{-1}(V) \in \tau _1 \)
then show \( f \text{ is continuous } \) using IsContinuous_def
qed
We can strenghten the previous lemma: it is sufficient to check if the inverse image of every set in a subbase is open. The proof is rather awkward, as usual when we deal with general intersections. We have to keep track of the case when the collection is empty.
lemma (in two_top_spaces0) Top_ZF_2_1_L6:
assumes A1: \( B \text{ is a subbase for } \tau _2 \) and A2: \( \forall U\in B.\ f^{-1}(U) \in \tau _1 \)
shows \( f \text{ is continuous } \)proof let \( C = \{\bigcap A.\ A \in \text{FinPow}(B)\} \)
from A1 have \( C \text{ is a base for } \tau _2 \) using IsAsubBaseFor_def
moreover
qed
have \( \forall U\in C.\ f^{-1}(U) \in \tau _1 \)proof
}
ultimately show \( f \text{ is continuous } \) using Top_ZF_2_1_L5
fix \( U \)
assume \( U\in C \)
{
assume \( f^{-1}(U) = 0 \)
with tau1_is_top have \( f^{-1}(U) \in \tau _1 \) using empty_open
moreover {
}
ultimately show \( f^{-1}(U) \in \tau _1 \)
qed
assume \( f^{-1}(U) \neq 0 \)
then have \( U\neq 0 \) by (rule func1_1_L13 )
moreover
from \( U\in C \) obtain \( A \) where \( A \in \text{FinPow}(B) \) and \( U = \bigcap A \)
ultimately have \( \bigcap A\neq 0 \)
then have \( A\neq 0 \) by (rule inter_nempty_nempty )
then have \( \{f^{-1}(W).\ W\in A\} \neq 0 \)
moreover
from A2, \( A \in \text{FinPow}(B) \) have \( \{f^{-1}(W).\ W\in A\} \in \text{FinPow}(\tau _1) \) by (rule fin_image_fin )
ultimately have \( \bigcap \{f^{-1}(W).\ W\in A\} \in \tau _1 \) using topol_cntxs_valid, fin_inter_open_open
moreover
from \( A \in \text{FinPow}(B) \) have \( A \subseteq B \) using FinPow_def
with tau2_is_top, A1 have \( A \subseteq Pow(X_2) \) using IsAsubBaseFor_def, IsATopology_def
with fmapAssum, \( A\neq 0 \), \( U = \bigcap A \) have \( f^{-1}(U) = \bigcap \{f^{-1}(W).\ W\in A\} \) using func1_1_L12
ultimately have \( f^{-1}(U) \in \tau _1 \)
A dual of Top_ZF_2_1_L5: a function that maps base sets to open sets is open.
lemma (in two_top_spaces0) base_image_open:
assumes A1: \( \mathcal{B} \text{ is a base for } \tau _1 \) and A2: \( \forall B\in \mathcal{B} .\ f(B) \in \tau _2 \) and A3: \( U\in \tau _1 \)
shows \( f(U) \in \tau _2 \)proof from A1, A3 obtain \( \ \lt E> \) where \( \ \lt E> \in Pow(\mathcal{B} ) \) and \( U = \bigcup \ \lt E> \) using Top_1_2_L1
with A1 have \( f(U) = \bigcup \{f(E).\ E \in \ \lt E>\} \) using Top_1_2_L5, fmapAssum, image_of_Union
moreover
qed
from A2, \( \ \lt E> \in Pow(\mathcal{B} ) \) have \( \{f(E).\ E \in \ \lt E>\} \in Pow(\tau _2) \)
then have \( \bigcup \{f(E).\ E \in \ \lt E>\} \in \tau _2 \) using tau2_is_top, IsATopology_def
ultimately show \( thesis \) using tau2_is_top, IsATopology_def
A composition of two continuous functions is continuous.
lemma comp_cont:
assumes \( \text{IsContinuous}(T,S,f) \) and \( \text{IsContinuous}(S,R,g) \)
shows \( \text{IsContinuous}(T,R,g\circ f) \) using assms, IsContinuous_def, vimage_compA composition of three continuous functions is continuous.
lemma comp_cont3:
assumes \( \text{IsContinuous}(T,S,f) \) and \( \text{IsContinuous}(S,R,g) \) and \( \text{IsContinuous}(R,P,h) \)
shows \( \text{IsContinuous}(T,P,h\circ g\circ f) \) using assms, IsContinuous_def, vimage_compThe graph of a continuous function into a Hausdorff topological space is closed in the product topology. Recall that in ZF a function is the same as its graph.
lemma (in two_top_spaces0) into_T2_graph_closed:
assumes \( f \text{ is continuous } \), \( \tau _2 \text{ is }T_2 \)
shows \( f \text{ is closed in } \text{ProductTopology}(\tau _1,\tau _2) \)proof from fmapAssum have \( f = \{\langle x,f(x)\rangle .\ x\in X_1\} \) using fun_is_set_of_pairs
let \( f_c = X_1\times X_2 - f \)
have \( f_c \in \text{ProductTopology}(\tau _1,\tau _2) \)proof
{
}
fix \( p \)
assume \( p\in f_c \)
then have \( p \in X_1\times X_2 \) and \( p \notin f \)
from \( p\in X_1\times X_2 \) obtain \( x \) \( y \) where \( x\in X_1 \), \( y\in X_2 \), \( p = \langle x,y\rangle \)
have \( y\neq f(x) \)proof
{
}
assume \( y=f(x) \)
with \( x\in X_1 \), \( p = \langle x,y\rangle \) have \( p \in \{\langle x,f(x)\rangle .\ x\in X_1\} \)
with \( f = \{\langle x,f(x)\rangle .\ x\in X_1\} \), \( p \notin f \) have \( False \)
thus \( y\neq f(x) \)
qed
from fmapAssum, \( x\in X_1 \) have \( f(x) \in X_2 \) by (rule apply_funtype )
with \( y\in X_2 \) have \( y\in \bigcup \tau _2 \), \( f(x) \in \bigcup \tau _2 \)
with assms(2), \( y\neq f(x) \) obtain \( U \) \( V \) where \( U\in \tau _2 \), \( V\in \tau _2 \), \( y\in U \), \( f(x)\in V \), \( U\cap V = 0 \) unfolding isT2_def
let \( W = f^{-1}(V) \)
have \( W\in \tau _1 \), \( W\subseteq X_1 \), \( U\subseteq X_2 \), \( x\in W \), \( p\in W\times U \), \( f(W) \subseteq V \)proof
from assms(1) have \( \text{IsContinuous}(\tau _1,\tau _2,f) \)
with \( V\in \tau _2 \), \( U\in \tau _2 \) show \( W\in \tau _1 \), \( W\subseteq X_1 \), \( U\subseteq X_2 \) unfolding IsContinuous_def
from fmapAssum, \( x\in X_1 \), \( f(x)\in V \) show \( x\in W \) using func1_1_L15
with \( y\in U \), \( y\in U \), \( p = \langle x,y\rangle \) show \( p\in W\times U \)
from fmapAssum show \( f(W) \subseteq V \) using fun_is_fun, function_image_vimage
qed
from fmapAssum, \( U\cap V = 0 \), \( W\subseteq X_1 \), \( U\subseteq X_2 \) have \( W\times U \subseteq f_c \) using vimage_prod_dis_graph
with \( W\in \tau _1 \), \( U\in \tau _2 \), \( p\in W\times U \) have \( \exists W\in \tau _1.\ \exists U\in \tau _2.\ p\in W\times U \wedge W\times U \subseteq f_c \)
with tau1_is_top, tau2_is_top show \( f_c \in \text{ProductTopology}(\tau _1,\tau _2) \) using point_neighb_prod_top
qed
with fmapAssum, tau1_is_top, tau2_is_top show \( thesis \) using fun_subset_prod, Top_1_4_T1(3) unfolding IsClosed_def
qed
Homeomorphisms
This section studies ''homeomorphisms'' - continous bijections whose inverses are also continuous. Notions that are preserved by (commute with) homeomorphisms are called ''topological invariants''.
Homeomorphism is a bijection that preserves open sets.
definition
\( \text{IsAhomeomorphism}(T,S,f) \equiv \) \( f \in \text{bij}(\bigcup T,\bigcup S) \wedge \text{IsContinuous}(T,S,f) \wedge \text{IsContinuous}(S,T,converse(f)) \)
Inverse (converse) of a homeomorphism is a homeomorphism.
lemma homeo_inv:
assumes \( \text{IsAhomeomorphism}(T,S,f) \)
shows \( \text{IsAhomeomorphism}(S,T,converse(f)) \) using assms, IsAhomeomorphism_def, bij_converse_bij, bij_converse_converseHomeomorphisms are open maps.
lemma homeo_open:
assumes \( \text{IsAhomeomorphism}(T,S,f) \) and \( U\in T \)
shows \( f(U) \in S \) using assms, image_converse, IsAhomeomorphism_def, IsContinuous_defA continuous bijection that is an open map is a homeomorphism.
lemma bij_cont_open_homeo:
assumes \( f \in \text{bij}(\bigcup T,\bigcup S) \) and \( \text{IsContinuous}(T,S,f) \) and \( \forall U\in T.\ f(U) \in S \)
shows \( \text{IsAhomeomorphism}(T,S,f) \) using assms, image_converse, IsAhomeomorphism_def, IsContinuous_defA continuous bijection that maps base to open sets is a homeomorphism.
lemma (in two_top_spaces0) bij_base_open_homeo:
assumes A1: \( f \in \text{bij}(X_1,X_2) \) and A2: \( \mathcal{B} \text{ is a base for } \tau _1 \) and A3: \( \mathcal{C} \text{ is a base for } \tau _2 \) and A4: \( \forall U\in \mathcal{C} .\ f^{-1}(U) \in \tau _1 \) and A5: \( \forall V\in \mathcal{B} .\ f(V) \in \tau _2 \)
shows \( \text{IsAhomeomorphism}(\tau _1,\tau _2,f) \) using assms, tau2_is_top, tau1_is_top, bij_converse_bij, bij_is_fun, two_top_spaces0_def, image_converse, Top_ZF_2_1_L5, IsAhomeomorphism_defA bijection that maps base to base is a homeomorphism.
lemma (in two_top_spaces0) bij_base_homeo:
assumes A1: \( f \in \text{bij}(X_1,X_2) \) and A2: \( \mathcal{B} \text{ is a base for } \tau _1 \) and A3: \( \{f(B).\ B\in \mathcal{B} \} \text{ is a base for } \tau _2 \)
shows \( \text{IsAhomeomorphism}(\tau _1,\tau _2,f) \)proof note A1
moreover
qed
have \( f \text{ is continuous } \)proof
moreover {
}
fix \( C \)
assume \( C \in \{f(B).\ B\in \mathcal{B} \} \)
then obtain \( B \) where \( B\in \mathcal{B} \) and I: \( C = f(B) \)
with A2 have \( B \subseteq X_1 \) using Top_1_2_L5
with A1, A2, \( B\in \mathcal{B} \), I have \( f^{-1}(C) \in \tau _1 \) using bij_def, inj_vimage_image, base_sets_open
hence \( \forall C \in \{f(B).\ B\in \mathcal{B} \}.\ f^{-1}(C) \in \tau _1 \)
with A3 show \( thesis \) by (rule Top_ZF_2_1_L5 )
qed
from A3 have \( \forall B\in \mathcal{B} .\ f(B) \in \tau _2 \) using base_sets_open
with A2 have \( \forall U\in \tau _1.\ f(U) \in \tau _2 \) using base_image_open
ultimately show \( thesis \) using bij_cont_open_homeo
Interior is a topological invariant.
theorem int_top_invariant:
assumes A1: \( A\subseteq \bigcup T \) and A2: \( \text{IsAhomeomorphism}(T,S,f) \)
shows \( f( \text{Interior}(A,T)) = \text{Interior}(f(A),S) \)proof let \( \mathcal{A} = \{U\in T.\ U\subseteq A\} \)
have I: \( \{f(U).\ U\in \mathcal{A} \} = \{V\in S.\ V \subseteq f(A)\} \)proof
}
from A2 show \( \{f(U).\ U\in \mathcal{A} \} \subseteq \{V\in S.\ V \subseteq f(A)\} \) using homeo_open
{
fix \( V \)
assume \( V \in \{V\in S.\ V \subseteq f(A)\} \)
hence \( V\in S \) and II: \( V \subseteq f(A) \)
let \( U = f^{-1}(V) \)
from II have \( U \subseteq f^{-1}(f(A)) \)
moreover
from assms have \( f^{-1}(f(A)) = A \) using IsAhomeomorphism_def, bij_def, inj_vimage_image
moreover from A2, \( V\in S \) have \( U\in T \) using IsAhomeomorphism_def, IsContinuous_def
moreover from \( V\in S \) have \( V \subseteq \bigcup S \)
with A2 have \( V = f(U) \) using IsAhomeomorphism_def, bij_def, surj_image_vimage
ultimately have \( V \in \{f(U).\ U\in \mathcal{A} \} \)
thus \( \{V\in S.\ V \subseteq f(A)\} \subseteq \{f(U).\ U\in \mathcal{A} \} \)
qed
have \( f( \text{Interior}(A,T)) = f(\bigcup \mathcal{A} ) \) unfolding Interior_def
also
qed
from A2 have \( \ldots = \bigcup \{f(U).\ U\in \mathcal{A} \} \) using IsAhomeomorphism_def, bij_def, inj_def, image_of_Union
also from I have \( \ldots = \text{Interior}(f(A),S) \) unfolding Interior_def
finally show \( thesis \)
Topologies induced by mappings
In this section we consider various ways a topology may be defined on a set that is the range (or the domain) of a function whose domain (or range) is a topological space.
A bijection from a topological space induces a topology on the range.
theorem bij_induced_top:
assumes A1: \( T \text{ is a topology } \) and A2: \( f \in \text{bij}(\bigcup T,Y) \)
shows \( \{f(U).\ U\in T\} \text{ is a topology } \) and \( \{ \{f(x).\ x\in U\}.\ U\in T\} \text{ is a topology } \) and \( (\bigcup \{f(U).\ U\in T\}) = Y \) and \( \text{IsAhomeomorphism}(T, \{f(U).\ U\in T\},f) \)proof from A2 have \( f \in \text{inj}(\bigcup T,Y) \) using bij_def
then have \( f:\bigcup T\rightarrow Y \) using inj_def
let \( S = \{f(U).\ U\in T\} \)
{
fix \( M \)
assume \( M \in Pow(S) \)
let \( M_T = \{f^{-1}(V).\ V\in M\} \)
have \( M_T \subseteq T \)proof
fix \( W \)
assume \( W\in M_T \)
then obtain \( V \) where \( V\in M \) and I: \( W = f^{-1}(V) \)
with \( M \in Pow(S) \) have \( V\in S \)
then obtain \( U \) where \( U\in T \) and \( V = f(U) \)
with I have \( W = f^{-1}(f(U)) \)
with \( f \in \text{inj}(\bigcup T,Y) \), \( U\in T \) have \( W = U \) using inj_vimage_image
with \( U\in T \) show \( W\in T \)
qed
with A1 have \( (\bigcup M_T) \in T \) using IsATopology_def
hence \( f(\bigcup M_T) \in S \)
moreover
have \( f(\bigcup M_T) = \bigcup M \)proof
ultimately have \( \bigcup M \in S \)
from \( f:\bigcup T\rightarrow Y \), \( M_T \subseteq T \) have \( f(\bigcup M_T) = \bigcup \{f(U).\ U\in M_T\} \) using image_of_Union
moreover
qed
have \( \{f(U).\ U\in M_T\} = M \)proof
ultimately show \( f(\bigcup M_T) = \bigcup M \)
from \( f:\bigcup T\rightarrow Y \) have \( \forall U\in T.\ f(U) \subseteq Y \) using func1_1_L6
with \( M \in Pow(S) \) have \( M \subseteq Pow(Y) \)
with A2 show \( \{f(U).\ U\in M_T\} = M \) using bij_def, surj_subsets
qed
then have \( \forall M\in Pow(S).\ \bigcup M \in S \)
moreover {
}
fix \( U \) \( V \)
assume \( U\in S \), \( V\in S \)
then obtain \( U_T \) \( V_T \) where \( U_T \in T \), \( V_T \in T \) and I: \( U = f(U_T) \), \( V = f(V_T) \)
with A1 have \( U_T\cap V_T \in T \) using IsATopology_def
hence \( f(U_T\cap V_T) \in S \)
moreover
have \( f(U_T\cap V_T) = U\cap V \)proof
ultimately have \( U\cap V \in S \)
from \( U_T \in T \), \( V_T \in T \) have \( U_T \subseteq \bigcup T \), \( V_T \subseteq \bigcup T \) using bij_def
with \( f \in \text{inj}(\bigcup T,Y) \), I show \( f(U_T\cap V_T) = U\cap V \) using inj_image_inter
qed
then have \( \forall U\in S.\ \forall V\in S.\ U\cap V \in S \)
ultimately show \( S \text{ is a topology } \) using IsATopology_def
moreover
from \( f:\bigcup T\rightarrow Y \) have \( \forall U\in T.\ f(U) = \{f(x).\ x\in U\} \) using func_imagedef
ultimately show \( \{ \{f(x).\ x\in U\}.\ U\in T\} \text{ is a topology } \)
show \( \bigcup S = Y \)proof
from \( f:\bigcup T\rightarrow Y \) have \( \forall U\in T.\ f(U) \subseteq Y \) using func1_1_L6
thus \( \bigcup S \subseteq Y \)
from A1 have \( f(\bigcup T) \subseteq \bigcup S \) using IsATopology_def
with A2 show \( Y \subseteq \bigcup S \) using bij_def, surj_range_image_domain
qed
show \( \text{IsAhomeomorphism}(T,S,f) \)proof
qed
from A2, \( \bigcup S = Y \) have \( f \in \text{bij}(\bigcup T,\bigcup S) \)
moreover
qed
have \( \text{IsContinuous}(T,S,f) \)proof
ultimately show \( \text{IsAhomeomorphism}(T,S,f) \) using bij_cont_open_homeo
{
}
fix \( V \)
assume \( V\in S \)
then obtain \( U \) where \( U\in T \) and \( V = f(U) \)
hence \( U \subseteq \bigcup T \) and \( f^{-1}(V) = f^{-1}(f(U)) \)
with \( f \in \text{inj}(\bigcup T,Y) \), \( U\in T \) have \( f^{-1}(V) \in T \) using inj_vimage_image
then show \( \text{IsContinuous}(T,S,f) \) unfolding IsContinuous_def
qed
Partial functions and continuity
Suppose we have two topologies \(\tau_1,\tau_2\) on sets \(X_i=\bigcup\tau_i, i=1,2\). Consider some function \(f:A\rightarrow X_2\), where \(A\subseteq X_1\) (we will call such function ''partial''). In such situation we have two natural possibilities for the pairs of topologies with respect to which this function may be continuous. One is obviously the original \(\tau_1,\tau_2\) and in the second one the first element of the pair is the topology relative to the domain of the function: \(\{A\cap U | U \in \tau_1\}\). These two possibilities are not exactly the same and the goal of this section is to explore the differences.
If a function is continuous, then its restriction is continous in relative topology.
lemma (in two_top_spaces0) restr_cont:
assumes A1: \( A \subseteq X_1 \) and A2: \( f \text{ is continuous } \)
shows \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2,\text{restrict}(f,A)) \)proof let \( g = \text{restrict}(f,A) \)
{
fix \( U \)
assume \( U \in \tau _2 \)
with A2 have \( f^{-1}(U) \in \tau _1 \) using IsContinuous_def
moreover
from A1 have \( g^{-1}(U) = f^{-1}(U) \cap A \) using fmapAssum, func1_2_L1
ultimately have \( g^{-1}(U) \in (\tau _1 \text{ restricted to } A) \) using RestrictedTo_def
then show \( thesis \) using IsContinuous_def
qed
If a function is continuous, then it is continuous when we restrict the topology on the range to the image of the domain.
lemma (in two_top_spaces0) restr_image_cont:
assumes A1: \( f \text{ is continuous } \)
shows \( \text{IsContinuous}(\tau _1, \tau _2 \text{ restricted to } f(X_1),f) \)proof have \( \forall U \in \tau _2 \text{ restricted to } f(X_1).\ f^{-1}(U) \in \tau _1 \)proof
fix \( U \)
assume \( U \in \tau _2 \text{ restricted to } f(X_1) \)
then obtain \( V \) where \( V \in \tau _2 \) and \( U = V \cap f(X_1) \) using RestrictedTo_def
with A1 show \( f^{-1}(U) \in \tau _1 \) using fmapAssum, inv_im_inter_im, IsContinuous_def
qed
then show \( thesis \) using IsContinuous_def
qed
A combination of restr_cont and restr_image_cont.
lemma (in two_top_spaces0) restr_restr_image_cont:
assumes A1: \( A \subseteq X_1 \) and A2: \( f \text{ is continuous } \) and A3: \( g = \text{restrict}(f,A) \) and A4: \( \tau _3 = \tau _1 \text{ restricted to } A \)
shows \( \text{IsContinuous}(\tau _3, \tau _2 \text{ restricted to } g(A),g) \)proof from A1, A4 have \( \bigcup \tau _3 = A \) using union_restrict
have \( two\_top\_spaces0(\tau _3, \tau _2, g) \)proof
from A4 have \( \tau _3 \text{ is a topology } \) and \( \tau _2 \text{ is a topology } \) using tau1_is_top, tau2_is_top, topology0_def, Top_1_L4
moreover
qed
from A1, A3, \( \bigcup \tau _3 = A \) have \( g: \bigcup \tau _3 \rightarrow \bigcup \tau _2 \) using fmapAssum, restrict_type2
ultimately show \( thesis \) using two_top_spaces0_def
moreover
from assms have \( \text{IsContinuous}(\tau _3, \tau _2, g) \) using restr_cont
ultimately have \( \text{IsContinuous}(\tau _3, \tau _2 \text{ restricted to } g(\bigcup \tau _3),g) \) by (rule restr_image_cont )
moreover
qed
note \( \bigcup \tau _3 = A \)
ultimately show \( thesis \)
We need a context similar to two_top_spaces0 but without the global function \(f:X_1\rightarrow X_2\).
locale two_top_spaces1
assumes tau1_is_top: \( \tau _1 \text{ is a topology } \)
assumes tau2_is_top: \( \tau _2 \text{ is a topology } \)
defines \( X_1 \equiv \bigcup \tau _1 \)
defines \( X_2 \equiv \bigcup \tau _2 \)
If a partial function \(g:X_1\supseteq A\rightarrow X_2\) is continuous with respect to \((\tau_1,\tau_2)\), then \(A\) is open (in \(\tau_1\)) and the function is continuous in the relative topology.
lemma (in two_top_spaces1) partial_fun_cont:
assumes A1: \( g:A\rightarrow X_2 \) and A2: \( \text{IsContinuous}(\tau _1,\tau _2,g) \)
shows \( A \in \tau _1 \) and \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \)proof from A2 have \( g^{-1}(X_2) \in \tau _1 \) using tau2_is_top, IsATopology_def, IsContinuous_def
with A1 show \( A \in \tau _1 \) using func1_1_L4
{
fix \( V \)
assume \( V \in \tau _2 \)
with A2 have \( g^{-1}(V) \in \tau _1 \) using IsContinuous_def
moreover
from A1 have \( g^{-1}(V) \subseteq A \) using func1_1_L3
hence \( g^{-1}(V) = A \cap g^{-1}(V) \)
ultimately have \( g^{-1}(V) \in (\tau _1 \text{ restricted to } A) \) using RestrictedTo_def
then show \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \) using IsContinuous_def
qed
For partial function defined on open sets continuity in the whole and relative topologies are the same.
lemma (in two_top_spaces1) part_fun_on_open_cont:
assumes A1: \( g:A\rightarrow X_2 \) and A2: \( A \in \tau _1 \)
shows \( \text{IsContinuous}(\tau _1,\tau _2,g) \longleftrightarrow \) \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \)proof assume \( \text{IsContinuous}(\tau _1,\tau _2,g) \)
with A1 show \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \) using partial_fun_cont
next
assume I: \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \)
{
fix \( V \)
assume \( V \in \tau _2 \)
with I have \( g^{-1}(V) \in (\tau _1 \text{ restricted to } A) \) using IsContinuous_def
then obtain \( W \) where \( W \in \tau _1 \) and \( g^{-1}(V) = A\cap W \) using RestrictedTo_def
with A2 have \( g^{-1}(V) \in \tau _1 \) using tau1_is_top, IsATopology_def
then show \( \text{IsContinuous}(\tau _1,\tau _2,g) \) using IsContinuous_def
qed
Product topology and continuity
We start with three topological spaces \((\tau_1,X_1), (\tau_2,X_2)\) and \((\tau_3,X_3)\) and a function \(f:X_1\times X_2\rightarrow X_3\). We will study the properties of \(f\) with respect to the product topology \(\tau_1\times \tau_2\) and \(\tau_3\). This situation is similar as in locale two_top_spaces0 but the first topological space is assumed to be a product of two topological spaces.
First we define a locale with three topological spaces.
locale prod_top_spaces0
assumes tau1_is_top: \( \tau _1 \text{ is a topology } \)
assumes tau2_is_top: \( \tau _2 \text{ is a topology } \)
assumes tau3_is_top: \( \tau _3 \text{ is a topology } \)
defines \( X_1 \equiv \bigcup \tau _1 \)
defines \( X_2 \equiv \bigcup \tau _2 \)
defines \( X_3 \equiv \bigcup \tau _3 \)
defines \( \eta \equiv \text{ProductTopology}(\tau _1,\tau _2) \)
Fixing the first variable in a two-variable continuous function results in a continuous function.
lemma (in prod_top_spaces0) fix_1st_var_cont:
assumes \( f: X_1\times X_2\rightarrow X_3 \) and \( \text{IsContinuous}(\eta ,\tau _3,f) \) and \( x\in X_1 \)
shows \( \text{IsContinuous}(\tau _2,\tau _3, \text{Fix1stVar}(f,x)) \) using assms, fix_1st_var_vimage, IsContinuous_def, tau1_is_top, tau2_is_top, prod_sec_open1Fixing the second variable in a two-variable continuous function results in a continuous function.
lemma (in prod_top_spaces0) fix_2nd_var_cont:
assumes \( f: X_1\times X_2\rightarrow X_3 \) and \( \text{IsContinuous}(\eta ,\tau _3,f) \) and \( y\in X_2 \)
shows \( \text{IsContinuous}(\tau _1,\tau _3, \text{Fix2ndVar}(f,y)) \) using assms, fix_2nd_var_vimage, IsContinuous_def, tau1_is_top, tau2_is_top, prod_sec_open2Having two constinuous mappings we can construct a third one on the cartesian product of the domains.
lemma cart_prod_cont:
assumes A1: \( \tau _1 \text{ is a topology } \), \( \tau _2 \text{ is a topology } \) and A2: \( \eta _1 \text{ is a topology } \), \( \eta _2 \text{ is a topology } \) and A3a: \( f_1:\bigcup \tau _1\rightarrow \bigcup \eta _1 \) and A3b: \( f_2:\bigcup \tau _2\rightarrow \bigcup \eta _2 \) and A4: \( \text{IsContinuous}(\tau _1,\eta _1,f_1) \), \( \text{IsContinuous}(\tau _2,\eta _2,f_2) \) and A5: \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)
shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _2), \text{ProductTopology}(\eta _1,\eta _2),g) \)proof let \( \tau = \text{ProductTopology}(\tau _1,\tau _2) \)
let \( \eta = \text{ProductTopology}(\eta _1,\eta _2) \)
let \( X_1 = \bigcup \tau _1 \)
let \( X_2 = \bigcup \tau _2 \)
let \( Y_1 = \bigcup \eta _1 \)
let \( Y_2 = \bigcup \eta _2 \)
let \( B = \text{ProductCollection}(\eta _1,\eta _2) \)
from A1, A2 have \( \tau \text{ is a topology } \) and \( \eta \text{ is a topology } \) using Top_1_4_T1
moreover
have \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \)proof
moreover {
}
fix \( p \)
assume \( p \in X_1\times X_2 \)
hence \( \text{fst}(p) \in X_1 \) and \( \text{snd}(p) \in X_2 \)
from A3a, \( \text{fst}(p) \in X_1 \) have \( f_1(\text{fst}(p)) \in Y_1 \) by (rule apply_funtype )
moreover
from A3b, \( \text{snd}(p) \in X_2 \) have \( f_2(\text{snd}(p)) \in Y_2 \) by (rule apply_funtype )
ultimately have \( \langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \in \bigcup \eta _1\times \bigcup \eta _2 \)
hence \( \forall p \in X_1\times X_2.\ \langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \in Y_1\times Y_2 \)
with A5 show \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \) using ZF_fun_from_total
qed
from A1, A2 have \( \bigcup \tau = X_1\times X_2 \) and \( \bigcup \eta = Y_1\times Y_2 \) using Top_1_4_T1
ultimately have \( two\_top\_spaces0(\tau ,\eta ,g) \) using two_top_spaces0_def
moreover
qed
from A2 have \( B \text{ is a base for } \eta \) using Top_1_4_T1
moreover have \( \forall U\in B.\ g^{-1}(U) \in \tau \)proof
ultimately show \( thesis \) using Top_ZF_2_1_L5
fix \( U \)
assume \( U\in B \)
then obtain \( V \) \( W \) where \( V \in \eta _1 \), \( W \in \eta _2 \) and \( U = V\times W \) using ProductCollection_def
with A3a, A3b, A5 have \( g^{-1}(U) = f_1^{-1}(V) \times f_2^{-1}(W) \) using cart_prod_fun_vimage
moreover
qed
from A1, A4, \( V \in \eta _1 \), \( W \in \eta _2 \) have \( f_1^{-1}(V) \times f_2^{-1}(W) \in \tau \) using IsContinuous_def, prod_open_open_prod
ultimately show \( g^{-1}(U) \in \tau \)
A reformulation of the cart_prod_cont lemma above in slightly different notation.
theorem (in two_top_spaces0) product_cont_functions:
assumes \( f:X_1\rightarrow X_2 \), \( g:\bigcup \tau _3\rightarrow \bigcup \tau _4 \), \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( \text{IsContinuous}(\tau _3,\tau _4,g) \), \( \tau _4\text{ is a topology } \), \( \tau _3\text{ is a topology } \)
shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _3), \text{ProductTopology}(\tau _2,\tau _4),\{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times \bigcup \tau _3\}) \)proof have \( \{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times \bigcup \tau _3\} = \{\langle p,\langle f(\text{fst}(p)),g(\text{snd}(p))\rangle \rangle .\ p \in X_1\times \bigcup \tau _3\} \)
with tau1_is_top, tau2_is_top, assms show \( thesis \) using cart_prod_cont
qed
A special case of cart_prod_cont when the function acting on the second axis is the identity.
lemma cart_prod_cont1:
assumes A1: \( \tau _1 \text{ is a topology } \) and A1a: \( \tau _2 \text{ is a topology } \) and A2: \( \eta _1 \text{ is a topology } \) and A3: \( f_1:\bigcup \tau _1\rightarrow \bigcup \eta _1 \) and A4: \( \text{IsContinuous}(\tau _1,\eta _1,f_1) \) and A5: \( g = \{\langle p, \langle f_1(\text{fst}(p)),\text{snd}(p)\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)
shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _2), \text{ProductTopology}(\eta _1,\tau _2),g) \)proof let \( f_2 = id(\bigcup \tau _2) \)
have \( \forall x\in \bigcup \tau _2.\ f_2(x) = x \) using id_conv
hence I: \( \forall p \in \bigcup \tau _1\times \bigcup \tau _2.\ \text{snd}(p) = f_2(\text{snd}(p)) \)
note A1, A1a, A2, A1a, A3
moreover
qed
have \( f_2:\bigcup \tau _2\rightarrow \bigcup \tau _2 \) using id_type
moreover note A4
moreover have \( \text{IsContinuous}(\tau _2,\tau _2,f_2) \) using id_cont
moreover have \( g = \{\langle p, \langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)proof
ultimately show \( thesis \) by (rule cart_prod_cont )
from A5, I show \( g \subseteq \{\langle p, \langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)
from A5, I show \( \{\langle p, \langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \subseteq g \)
qed
Having two continuous mappings \(f,g\) we can construct a third one with values in the cartesian product of the codomains of \(f,g\), defined by \(x\mapsto \langle f(x),g(x) \rangle\).
lemma (in prod_top_spaces0) cont_funcs_prod:
assumes \( f:X_1\rightarrow X_2 \), \( g:X_1\rightarrow X_3 \), \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( \text{IsContinuous}(\tau _1,\tau _3,g) \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X_1\} \)
shows \( \text{IsContinuous}(\tau _1, \text{ProductTopology}(\tau _2,\tau _3),h) \)proof let \( B = \text{ProductCollection}(\tau _2,\tau _3) \)
have \( two\_top\_spaces0(\tau _1, \text{ProductTopology}(\tau _2,\tau _3),h) \), \( B \text{ is a base for } \text{ProductTopology}(\tau _2,\tau _3) \), \( \forall W\in B.\ h^{-1}(W) \in \tau _1 \)proof
from tau1_is_top, tau2_is_top, tau3_is_top, assms(1,2,5) show \( two\_top\_spaces0(\tau _1, \text{ProductTopology}(\tau _2,\tau _3),h) \) using vimage_prod, Top_1_4_T1(1,3) unfolding two_top_spaces0_def
from tau2_is_top, tau3_is_top show \( B \text{ is a base for } \text{ProductTopology}(\tau _2,\tau _3) \) using Top_1_4_T1(2)
from tau1_is_top, assms show \( \forall W\in B.\ h^{-1}(W) \in \tau _1 \) unfolding ProductCollection_def, IsContinuous_def, IsATopology_def using vimage_prod
qed
then show \( thesis \) by (rule Top_ZF_2_1_L5 )
qed
Having two continuous mappings \(f,g\) we can construct a third one with values in the cartesian product of the codomains of \(f,g\), defined by \(x\mapsto \langle f(x),g(x) \rangle\). This is essentially the same as cont_funcs_prod but formulated in a way that is sometimes easier to apply. Recall that \(\tau_2 \times_t \tau_3\) is a notation for the product topology of \(\tau_1\) and \(\tau_2\).
lemma cont_funcs_prod1:
assumes \( \tau _1 \text{ is a topology } \), \( \tau _2 \text{ is a topology } \), \( \tau _3 \text{ is a topology } \) and \( \{\langle x,p(x)\rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _2) \), \( \{\langle x,q(x)\rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _3) \)
shows \( \{\langle x,\langle p(x),q(x)\rangle \rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _2\times _t\tau _3) \)proof let \( X = \bigcup \tau _1 \)
let \( Y = \bigcup \tau _2 \)
let \( Z = \bigcup \tau _3 \)
let \( f = \{\langle x,p(x)\rangle .\ x\in X\} \)
let \( g = \{\langle x,q(x)\rangle .\ x\in X\} \)
let \( h = \{\langle x,\langle p(x),q(x)\rangle \rangle .\ x\in X\} \)
from assms(4,5) have \( f:X\rightarrow Y \) and \( g:X\rightarrow Z \) unfolding Cont_def
with assms(2,3) have hFun: \( h:X\rightarrow \bigcup (\tau _2\times _t\tau _3) \) using prod_fun_val(1) using Top_1_4_T1(3)
moreover
qed
have \( \text{IsContinuous}(\tau _1,\tau _2\times _t\tau _3,h) \)proof
ultimately show \( thesis \) unfolding Cont_def
let \( B = \text{ProductCollection}(\tau _2,\tau _3) \)
from assms(1,2,3), hFun have \( two\_top\_spaces0(\tau _1,\tau _2\times _t\tau _3,h) \) using Top_1_4_T1(1) unfolding two_top_spaces0_def
moreover
qed
from assms(2,3) have \( B \text{ is a base for } (\tau _2\times _t\tau _3) \) using Top_1_4_T1(2)
moreover have \( \forall W\in B.\ h^{-1}(W) \in \tau _1 \)proof
ultimately show \( thesis \) by (rule Top_ZF_2_1_L5 )
{
}
fix \( W \)
assume \( W\in B \)
then obtain \( U \) \( V \) where \( U\in \tau _2 \), \( V\in \tau _3 \), \( W=U\times V \) unfolding ProductCollection_def
have \( \forall x\in X.\ \langle p(x),q(x)\rangle = \langle f(x),g(x)\rangle \)proof
{
}
fix \( x \)
assume \( x\in X \)
then have \( \langle p(x),q(x)\rangle = \langle f(x),g(x)\rangle \) using ZF_fun_from_tot_val1
thus \( thesis \)
qed
then have \( h = \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \) by (rule set_comp_eq )
with assms(1,4,5), \( f:X\rightarrow Y \), \( g:X\rightarrow Z \), \( U\in \tau _2 \), \( V\in \tau _3 \), \( W=U\times V \) have \( h^{-1}(W) \in \tau _1 \) using vimage_prod(3) unfolding Cont_def, IsContinuous_def, IsATopology_def
thus \( thesis \)
qed
Two continuous functions into a Hausdorff space are equal on a closed set. Note that in the lemma below \(f\) is assumed to map \(X_1\) to \(X_2\) in the locale, we only need to add a similar assumption for the second function.
lemma (in two_top_spaces0) two_fun_eq_closed:
assumes \( g:X_1\rightarrow X_2 \), \( f \text{ is continuous } \), \( g \text{ is continuous } \), \( \tau _2 \text{ is }T_2 \)
shows \( \{x\in X_1.\ f(x)=g(x)\} \text{ is closed in } \tau _1 \)proof let \( D = \{x\in X_1.\ f(x)=g(x)\} \)
let \( h = \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X_1\} \)
have \( h^{-1}(\{\langle y,y\rangle .\ y\in X_2\}) \text{ is closed in } \tau _1 \)proof
have \( two\_top\_spaces0(\tau _1, \text{ProductTopology}(\tau _2,\tau _2),h) \)proof
from tau1_is_top, tau2_is_top show \( \tau _1 \text{ is a topology } \) and \( \text{ProductTopology}(\tau _2,\tau _2) \text{ is a topology } \) using Top_1_4_T1(1)
from tau1_is_top, tau2_is_top, fmapAssum, assms(1) show \( h : \bigcup \tau _1 \rightarrow \bigcup \text{ProductTopology}(\tau _2, \tau _2) \) using vimage_prod(1), Top_1_4_T1(3)
qed
moreover
qed
have \( \text{IsContinuous}(\tau _1, \text{ProductTopology}(\tau _2,\tau _2),h) \)proof
moreover from tau1_is_top, tau2_is_top have \( prod\_top\_spaces0(\tau _1,\tau _2,\tau _2) \) unfolding prod_top_spaces0_def
with fmapAssum, assms(1,2,3) show \( thesis \) using cont_funcs_prod
qed
from tau2_is_top, assms(4) have \( \{\langle y,y\rangle .\ y\in X_2\} \text{ is closed in } \text{ProductTopology}(\tau _2,\tau _2) \) using t2_iff_diag_closed
ultimately show \( thesis \) using TopZF_2_1_L1
with fmapAssum, assms(1) show \( thesis \) using vimage_prod(4)
qed
Closure of an image of a singleton by a relation in \(X\times Y\) is contained in the image of this singleton by the closure of the relation (in the product topology). Compare the proof of Metamath's theorem with the same name.
lemma imasncls:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \), \( R \subseteq (\bigcup T)\times (\bigcup S) \), \( x\in \bigcup T \)
shows \( \text{Closure}(R\{x\},S) \subseteq \text{Closure}(R,T\times _tS)\{x\} \)proof let \( X = \bigcup T \)
let \( Y = \bigcup S \)
let \( f = \{\langle y,\langle x,y\rangle \rangle .\ y\in Y\} \)
from assms(3) have \( R\{x\} = f^{-1}(R) \)
hence \( \text{Closure}(R\{x\},S) = \text{Closure}(f^{-1}(R),S) \)
also
qed
have \( \text{Closure}(f^{-1}(R),S) \subseteq f^{-1}( \text{Closure}(R,T\times _tS)) \)proof
also from assms(1,2,4) have \( f \in \text{Cont}(S,T\times _tS) \) using const_cont_sp, id_cont_sp, cont_funcs_prod1
with assms(1,2,3) have \( two\_top\_spaces0(S,T\times _tS,f) \), \( \text{IsContinuous}(S,T\times _tS,f) \), \( R \subseteq \bigcup (T\times _tS) \) unfolding Cont_def, two_top_spaces0_def using Top_1_4_T1(1,3)
then show \( \text{Closure}(f^{-1}(R),S) \subseteq f^{-1}( \text{Closure}(R,T\times _tS)) \) using im_cl_in_cl_im
qed
have \( \text{Closure}(R,T\times _tS) \subseteq X\times Y \)proof
from assms(1,2,3) have \( topology0(T\times _tS) \), \( R \subseteq \bigcup (T\times _tS) \) unfolding topology0_def using Top_1_4_T1(1,3)
then have \( \text{Closure}(R,T\times _tS) \subseteq \bigcup (T\times _tS) \) by (rule Top_3_L11 )
with assms(1,2) show \( thesis \) using Top_1_4_T1(3)
qed
with assms(4) have \( f^{-1}( \text{Closure}(R,T\times _tS)) = \text{Closure}(R,T\times _tS)\{x\} \)
finally show \( \text{Closure}(R\{x\},S) \subseteq \text{Closure}(R,T\times _tS)\{x\} \)
Pasting lemma
The classical pasting lemma states that if \(U_1,U_2\) are both open (or closed) and a function is continuous when restricted to both \(U_1\) and \(U_2\) then it is continuous when restricted to \(U_1 \cup U_2\). In this section we prove a generalization statement stating that the set \(\{ U \in \tau_1 | f|_U\) is continuous \(\}\) is a topology.
A typical statement of the pasting lemma uses the notion of a function restricted to a set being continuous without specifying the topologies with respect to which this continuity holds. In two_top_spaces0 context the notation \( g \text{ is continuous } \) means continuity wth respect to topologies \(\tau_1, \tau_2\). The next lemma is a special case of partial_fun_cont and states that if for some set \(A\subseteq X_1=\bigcup \tau_1\) the function \(f|_A\) is continuous (with respect to \((\tau_1, \tau_2)\)), then \(A\) has to be open. This clears up terminology and indicates why we need to pay attention to the issue of which topologies we talk about when we say that the restricted (to some closed set for example) function is continuos.
lemma (in two_top_spaces0) restriction_continuous1:
assumes A1: \( A \subseteq X_1 \) and A2: \( \text{restrict}(f,A) \text{ is continuous } \)
shows \( A \in \tau _1 \)proof from assms have \( two\_top\_spaces1(\tau _1,\tau _2) \) and \( \text{restrict}(f,A):A\rightarrow X_2 \) and \( \text{restrict}(f,A) \text{ is continuous } \) using tau1_is_top, tau2_is_top, two_top_spaces1_def, fmapAssum, restrict_fun
then show \( thesis \) using partial_fun_cont
qed
If a fuction is continuous on each set of a collection of open sets, then it is continuous on the union of them. We could use continuity with respect to the relative topology here, but we know that on open sets this is the same as the original topology.
lemma (in two_top_spaces0) pasting_lemma1:
assumes A1: \( M \subseteq \tau _1 \) and A2: \( \forall U\in M.\ \text{restrict}(f,U) \text{ is continuous } \)
shows \( \text{restrict}(f,\bigcup M) \text{ is continuous } \)proof{
}
fix \( V \)
assume \( V\in \tau _2 \)
from A1 have \( \bigcup M \subseteq X_1 \)
then have \( \text{restrict}(f,\bigcup M)^{-1}(V) = f^{-1}(V) \cap (\bigcup M) \) using func1_2_L1, fmapAssum
also
have \( \ldots = \bigcup \{f^{-1}(V) \cap U.\ U\in M\} \)
finally have \( \text{restrict}(f,\bigcup M)^{-1}(V) = \bigcup \{f^{-1}(V) \cap U.\ U\in M\} \)
moreover
have \( \{f^{-1}(V) \cap U.\ U\in M\} \in Pow(\tau _1) \)proof
{
}
fix \( W \)
assume \( W \in \{f^{-1}(V) \cap U.\ U\in M\} \)
then obtain \( U \) where \( U\in M \) and I: \( W = f^{-1}(V) \cap U \)
with A2 have \( \text{restrict}(f,U) \text{ is continuous } \)
with \( V\in \tau _2 \) have \( \text{restrict}(f,U)^{-1}(V) \in \tau _1 \) using IsContinuous_def
moreover
from \( \bigcup M \subseteq X_1 \), and, \( U\in M \) have \( \text{restrict}(f,U)^{-1}(V) = f^{-1}(V) \cap U \) using fmapAssum, func1_2_L1
ultimately have \( f^{-1}(V) \cap U \in \tau _1 \)
with I have \( W \in \tau _1 \)
then show \( thesis \)
qed
then have \( \bigcup \{f^{-1}(V) \cap U.\ U\in M\} \in \tau _1 \) using tau1_is_top, IsATopology_def
ultimately have \( \text{restrict}(f,\bigcup M)^{-1}(V) \in \tau _1 \)
then show \( thesis \) using IsContinuous_def
qed
If a function is continuous on two sets, then it is continuous on intersection.
lemma (in two_top_spaces0) cont_inter_cont:
assumes A1: \( A \subseteq X_1 \), \( B \subseteq X_1 \) and A2: \( \text{restrict}(f,A) \text{ is continuous } \), \( \text{restrict}(f,B) \text{ is continuous } \)
shows \( \text{restrict}(f,A\cap B) \text{ is continuous } \)proof{
}
fix \( V \)
assume \( V\in \tau _2 \)
with assms have \( \text{restrict}(f,A)^{-1}(V) = f^{-1}(V) \cap A \), \( \text{restrict}(f,B)^{-1}(V) = f^{-1}(V) \cap B \) and \( \text{restrict}(f,A)^{-1}(V) \in \tau _1 \) and \( \text{restrict}(f,B)^{-1}(V) \in \tau _1 \) using func1_2_L1, fmapAssum, IsContinuous_def
then have \( (\text{restrict}(f,A)^{-1}(V)) \cap (\text{restrict}(f,B)^{-1}(V)) = f^{-1}(V) \cap (A\cap B) \)
moreover
from A2, \( V\in \tau _2 \) have \( \text{restrict}(f,A)^{-1}(V) \in \tau _1 \) and \( \text{restrict}(f,B)^{-1}(V) \in \tau _1 \) using IsContinuous_def
then have \( (\text{restrict}(f,A)^{-1}(V)) \cap (\text{restrict}(f,B)^{-1}(V)) \in \tau _1 \) using tau1_is_top, IsATopology_def
moreover from A1 have \( (A\cap B) \subseteq X_1 \)
then have \( \text{restrict}(f,A\cap B)^{-1}(V) = f^{-1}(V) \cap (A\cap B) \) using func1_2_L1, fmapAssum
ultimately have \( \text{restrict}(f,A\cap B)^{-1}(V) \in \tau _1 \)
then show \( thesis \) using IsContinuous_def
qed
The collection of open sets \(U\) such that \(f\) restricted to \(U\) is continuous, is a topology.
theorem (in two_top_spaces0) pasting_theorem:
shows \( \{U \in \tau _1.\ \text{restrict}(f,U) \text{ is continuous }\} \text{ is a topology } \)proof let \( T = \{U \in \tau _1.\ \text{restrict}(f,U) \text{ is continuous }\} \)
have \( \forall M\in Pow(T).\ \bigcup M \in T \)proof
fix \( M \)
assume \( M \in Pow(T) \)
then have \( \text{restrict}(f,\bigcup M) \text{ is continuous } \) using pasting_lemma1
with \( M \in Pow(T) \) show \( \bigcup M \in T \) using tau1_is_top, IsATopology_def
qed
moreover
qed
have \( \forall U\in T.\ \forall V\in T.\ U\cap V \in T \) using cont_inter_cont, tau1_is_top, IsATopology_def
ultimately show \( thesis \) using IsATopology_def
0 is continuous.
corollary (in two_top_spaces0) zero_continuous:
shows \( 0 \text{ is continuous } \)proof let \( T = \{U \in \tau _1.\ \text{restrict}(f,U) \text{ is continuous }\} \)
have \( T \text{ is a topology } \) by (rule pasting_theorem )
then have \( 0\in T \) by (rule empty_open )
hence \( \text{restrict}(f,0) \text{ is continuous } \)
moreover
qed
have \( \text{restrict}(f,0) = 0 \)
ultimately show \( thesis \)
end
lemma vimage_id_same:
assumes \( A\subseteq X \)
shows \( id(X)^{-1}(A) = A \)Definition of IsContinuous:
\( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
lemma id_cont: shows \( \text{IsContinuous}(\tau ,\tau ,id(\bigcup \tau )) \)
Definition of Cont:
\( \text{Cont}(\tau _1,\tau _2) \equiv \{f\in (\bigcup \tau _1)\rightarrow (\bigcup \tau _2).\ \text{IsContinuous}(\tau _1,\tau _2,f)\} \)
lemma carr_open:
assumes \( T \text{ is a topology } \)
shows \( (\bigcup T) \in T \) lemma const_vimage_domain:
assumes \( c\in A \)
shows \( \text{ConstantFunction}(X,c)^{-1}(A) = X \) lemma empty_open:
assumes \( T \text{ is a topology } \)
shows \( 0 \in T \) lemma const_vimage_empty:
assumes \( c\notin A \)
shows \( \text{ConstantFunction}(X,c)^{-1}(A) = \emptyset \) lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma const_fun_def_alt: shows \( \text{ConstantFunction}(X,c) = \{\langle x,c\rangle .\ x\in X\} \)
lemma const_cont:
assumes \( T \text{ is a topology } \)
shows \( \text{IsContinuous}(T,\tau , \text{ConstantFunction}(\bigcup T,c)) \) lemma func1_1_L3:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(D) \subseteq X \) lemma func1_1_L4:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(Y) = X \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
lemma (in two_top_spaces0) topol_cntxs_valid: shows \( topology0(\tau _1) \) and \( topology0(\tau _2) \)
lemma (in topology0) Top_3_L9:
assumes \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \) lemma func1_1_L6:
assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \) lemma (in topology0) cl_contains_set:
assumes \( A \subseteq \bigcup T \)
shows \( A \subseteq cl(A) \) lemma func1_1_L9:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( A \subseteq f^{-1}(f(A)) \) lemma func1_1_L8:
assumes \( A\subseteq B \)
shows \( f(A)\subseteq f(B) \) lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \) lemma (in topology0) Top_3_L13:
assumes \( B \text{ is closed in } T \), \( A\subseteq B \)
shows \( cl(A) \subseteq B \) lemma (in topology0) top_closure_mono:
assumes \( B \subseteq \bigcup T \) and \( A\subseteq B \)
shows \( cl(A) \subseteq cl(B) \) lemma (in topology0) Top_3_L8:
assumes \( A \subseteq \bigcup T \)
shows \( A \text{ is closed in } T \longleftrightarrow cl(A) = A \) lemma (in two_top_spaces0) TopZF_2_1_L1:
assumes \( f \text{ is continuous } \) and \( D \text{ is closed in } \tau _2 \)
shows \( f^{-1}(D) \text{ is closed in } \tau _1 \) lemma (in two_top_spaces0) Top_ZF_2_1_L2:
assumes \( \forall D.\ ((D \text{ is closed in } \tau _2) \longrightarrow f^{-1}(D) \text{ is closed in } \tau _1) \) and \( A \subseteq X_1 \)
shows \( f(cl_1(A)) \subseteq cl_2(f(A)) \) lemma (in two_top_spaces0) Top_ZF_2_1_L3:
assumes \( \forall A.\ ( A \subseteq X_1 \longrightarrow f(cl_1(A)) \subseteq cl_2(f(A))) \)
shows \( \forall B.\ ( B \subseteq X_2 \longrightarrow cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) ) \)Definition of IsAbaseFor:
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
Definition of IsAsubBaseFor:
\( B \text{ is a subbase for } T \equiv \)
\( B \subseteq T \wedge \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ is a base for } T \)
lemma func1_1_L13:
assumes \( f^{-1}(A) \neq \emptyset \)
shows \( A\neq \emptyset \) lemma inter_nempty_nempty:
assumes \( \bigcap A \neq \emptyset \)
shows \( A\neq \emptyset \) lemma fin_image_fin:
assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)
shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \) lemma (in topology0) fin_inter_open_open:
assumes \( N\neq 0 \), \( N \in \text{FinPow}(T) \)
shows \( \bigcap N \in T \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma func1_1_L12:
assumes \( B \subseteq Pow(Y) \) and \( B\neq \emptyset \) and \( f:X\rightarrow Y \)
shows \( f^{-1}(\bigcap B) = (\bigcap U\in B.\ f^{-1}(U)) \) lemma (in two_top_spaces0) Top_ZF_2_1_L5:
assumes \( B \text{ is a base for } \tau _2 \) and \( \forall U\in B.\ f^{-1}(U) \in \tau _1 \)
shows \( f \text{ is continuous } \) lemma Top_1_2_L1:
assumes \( B \text{ is a base for } T \) and \( U\in T \)
shows \( \exists A\in Pow(B).\ U = \bigcup A \) lemma Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \) lemma image_of_Union:
assumes \( f:X\rightarrow Y \) and \( \forall A\in M.\ A\subseteq X \)
shows \( f(\bigcup M) = \bigcup \{f(A).\ A\in M\} \) lemma vimage_comp: shows \( (r\circ s)^{-1}(A) = s^{-1}(r^{-1}(A)) \)
theorem fun_is_set_of_pairs:
assumes \( f:X\rightarrow Y \)
shows \( f = \{\langle x, f(x)\rangle .\ x \in X\} \)Definition of isT2:
\( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)
lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma fun_is_fun:
assumes \( f:X\rightarrow Y \)
shows \( function(f) \) lemma vimage_prod_dis_graph:
assumes \( f:X\rightarrow Y \), \( A\cap B = \emptyset \)
shows \( f^{-1}(A)\times B \cap f = \emptyset \) lemma point_neighb_prod_top:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( \forall p\in V.\ \exists U\in T.\ \exists W\in S.\ p\in U\times W \wedge U\times W \subseteq V \)
shows \( V \in \text{ProductTopology}(T,S) \) lemma fun_subset_prod:
assumes \( f:X\rightarrow Y \)
shows \( f \subseteq X\times Y \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \)Definition of IsAhomeomorphism:
\( \text{IsAhomeomorphism}(T,S,f) \equiv \)
\( f \in \text{bij}(\bigcup T,\bigcup S) \wedge \text{IsContinuous}(T,S,f) \wedge \text{IsContinuous}(S,T,converse(f)) \)
lemma bij_converse_converse:
assumes \( a \in \text{bij}(A,B) \)
shows \( converse(converse(a)) = a \) lemma image_converse: shows \( converse(r)^{-1}(A) = r(A) \)
lemma inj_vimage_image:
assumes \( f \in \text{inj}(X,Y) \) and \( A\subseteq X \)
shows \( f^{-1}(f(A)) = A \) lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \) lemma (in two_top_spaces0) base_image_open:
assumes \( \mathcal{B} \text{ is a base for } \tau _1 \) and \( \forall B\in \mathcal{B} .\ f(B) \in \tau _2 \) and \( U\in \tau _1 \)
shows \( f(U) \in \tau _2 \) lemma bij_cont_open_homeo:
assumes \( f \in \text{bij}(\bigcup T,\bigcup S) \) and \( \text{IsContinuous}(T,S,f) \) and \( \forall U\in T.\ f(U) \in S \)
shows \( \text{IsAhomeomorphism}(T,S,f) \) lemma homeo_open:
assumes \( \text{IsAhomeomorphism}(T,S,f) \) and \( U\in T \)
shows \( f(U) \in S \) lemma surj_image_vimage:
assumes \( f \in \text{surj}(X,Y) \) and \( A\subseteq Y \)
shows \( f(f^{-1}(A)) = A \)Definition of Interior:
\( \text{Interior}(A,T) \equiv \bigcup \{U\in T.\ U \subseteq A\} \)
lemma surj_subsets:
assumes \( f \in \text{surj}(X,Y) \) and \( B \subseteq Pow(Y) \)
shows \( \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} = B \) lemma inj_image_inter:
assumes \( f \in \text{inj}(X,Y) \) and \( A\subseteq X \), \( B\subseteq X \)
shows \( f(A\cap B) = f(A) \cap f(B) \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma surj_range_image_domain:
assumes \( f \in \text{surj}(A,B) \)
shows \( f(A) = B \) lemma func1_2_L1:
assumes \( f:X\rightarrow Y \) and \( B\subseteq X \)
shows \( \text{restrict}(f,B)^{-1}(A) = f^{-1}(A) \cap B \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
lemma inv_im_inter_im:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A \cap f(X)) = f^{-1}(A) \) lemma union_restrict: shows \( \bigcup (M \text{ restricted to } X) = (\bigcup M) \cap X \)
lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
lemma (in two_top_spaces0) restr_cont:
assumes \( A \subseteq X_1 \) and \( f \text{ is continuous } \)
shows \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2,\text{restrict}(f,A)) \) lemma (in two_top_spaces0) restr_image_cont:
assumes \( f \text{ is continuous } \)
shows \( \text{IsContinuous}(\tau _1, \tau _2 \text{ restricted to } f(X_1),f) \) lemma (in two_top_spaces1) partial_fun_cont:
assumes \( g:A\rightarrow X_2 \) and \( \text{IsContinuous}(\tau _1,\tau _2,g) \)
shows \( A \in \tau _1 \) and \( \text{IsContinuous}(\tau _1 \text{ restricted to } A, \tau _2, g) \) lemma fix_1st_var_vimage:
assumes \( f : X\times Y \rightarrow Z \) and \( x\in X \)
shows \( \text{Fix1stVar}(f,x)^{-1}(A) = \{y\in Y.\ \langle x,y\rangle \in f^{-1}(A)\} \) lemma prod_sec_open1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( V \in \text{ProductTopology}(T,S) \) and \( x \in \bigcup T \)
shows \( \{y \in \bigcup S.\ \langle x,y\rangle \in V\} \in S \) lemma fix_2nd_var_vimage:
assumes \( f : X\times Y \rightarrow Z \) and \( y\in Y \)
shows \( \text{Fix2ndVar}(f,y)^{-1}(A) = \{x\in X.\ \langle x,y\rangle \in f^{-1}(A)\} \) lemma prod_sec_open2:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( V \in \text{ProductTopology}(T,S) \) and \( y \in \bigcup S \)
shows \( \{x \in \bigcup T.\ \langle x,y\rangle \in V\} \in T \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \)Definition of ProductCollection:
\( \text{ProductCollection}(T,S) \equiv \bigcup U\in T.\ \{U\times V.\ V\in S\} \)
lemma cart_prod_fun_vimage:
assumes \( f_1:X_1\rightarrow Y_1 \), \( f_2:X_2\rightarrow Y_2 \) and \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in X_1\times X_2\} \)
shows \( g^{-1}(A_1\times A_2) = f_1^{-1}(A_1) \times f_2^{-1}(A_2) \) lemma prod_open_open_prod:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U\in T \), \( V\in S \)
shows \( U\times V \in \text{ProductTopology}(T,S) \) lemma cart_prod_cont:
assumes \( \tau _1 \text{ is a topology } \), \( \tau _2 \text{ is a topology } \) and \( \eta _1 \text{ is a topology } \), \( \eta _2 \text{ is a topology } \) and \( f_1:\bigcup \tau _1\rightarrow \bigcup \eta _1 \) and \( f_2:\bigcup \tau _2\rightarrow \bigcup \eta _2 \) and \( \text{IsContinuous}(\tau _1,\eta _1,f_1) \), \( \text{IsContinuous}(\tau _2,\eta _2,f_2) \) and \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in \bigcup \tau _1\times \bigcup \tau _2\} \)
shows \( \text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _2), \text{ProductTopology}(\eta _1,\eta _2),g) \) lemma vimage_prod:
assumes \( f:X\rightarrow Y \), \( g:X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \), \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \), \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \), \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma prod_fun_val:
assumes \( \{\langle x,p(x)\rangle .\ x\in X\}: X\rightarrow Y \), \( \{\langle x,q(x)\rangle .\ x\in X\}: X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle p(x),q(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \) and \( \forall x\in X.\ h(x) = \langle p(x),q(x)\rangle \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \) lemma set_comp_eq:
assumes \( \forall x\in X.\ p(x) = q(x) \)
shows \( \{p(x).\ x\in X\} = \{q(x).\ x\in X\} \) and \( \{\langle x,p(x)\rangle .\ x\in X\} = \{\langle x,q(x)\rangle .\ x\in X\} \) lemma vimage_prod:
assumes \( f:X\rightarrow Y \), \( g:X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \), \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \), \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \), \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \) lemma vimage_prod:
assumes \( f:X\rightarrow Y \), \( g:X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \), \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \), \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \), \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \) lemma (in prod_top_spaces0) cont_funcs_prod:
assumes \( f:X_1\rightarrow X_2 \), \( g:X_1\rightarrow X_3 \), \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( \text{IsContinuous}(\tau _1,\tau _3,g) \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X_1\} \)
shows \( \text{IsContinuous}(\tau _1, \text{ProductTopology}(\tau _2,\tau _3),h) \) theorem t2_iff_diag_closed:
assumes \( T \text{ is a topology } \)
shows \( T \text{ is }T_2 \longleftrightarrow \{\langle x,x\rangle .\ x\in \bigcup T\} \text{ is closed in } \text{ProductTopology}(T,T) \) lemma vimage_prod:
assumes \( f:X\rightarrow Y \), \( g:X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \), \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \), \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \), \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \) lemma const_cont_sp:
assumes \( T \text{ is a topology } \), \( c\in \bigcup S \)
shows \( \{\langle x,c\rangle .\ x\in \bigcup T\} \in \text{Cont}(T,S) \) lemma id_cont_sp: shows \( \{\langle x,x\rangle .\ x\in \bigcup \tau \} \in \text{Cont}(\tau ,\tau ) \)
lemma cont_funcs_prod1:
assumes \( \tau _1 \text{ is a topology } \), \( \tau _2 \text{ is a topology } \), \( \tau _3 \text{ is a topology } \) and \( \{\langle x,p(x)\rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _2) \), \( \{\langle x,q(x)\rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _3) \)
shows \( \{\langle x,\langle p(x),q(x)\rangle \rangle .\ x\in \bigcup \tau _1\} \in \text{Cont}(\tau _1,\tau _2\times _t\tau _3) \) corollary (in two_top_spaces0) im_cl_in_cl_im:
assumes \( f \text{ is continuous } \) and \( B \subseteq X_2 \)
shows \( cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) \) lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T - A) = \bigcup T - int(A) \) corollary restrict_fun:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( \text{restrict}(f,A) : A \rightarrow Y \) lemma (in two_top_spaces0) pasting_lemma1:
assumes \( M \subseteq \tau _1 \) and \( \forall U\in M.\ \text{restrict}(f,U) \text{ is continuous } \)
shows \( \text{restrict}(f,\bigcup M) \text{ is continuous } \) lemma (in two_top_spaces0) cont_inter_cont:
assumes \( A \subseteq X_1 \), \( B \subseteq X_1 \) and \( \text{restrict}(f,A) \text{ is continuous } \), \( \text{restrict}(f,B) \text{ is continuous } \)
shows \( \text{restrict}(f,A\cap B) \text{ is continuous } \) theorem (in two_top_spaces0) pasting_theorem: shows \( \{U \in \tau _1.\ \text{restrict}(f,U) \text{ is continuous }\} \text{ is a topology } \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8