theory Topology_ZF_2 imports Topology_ZF_1 func1 Fol1
begin
This theory continues the series on general topology and covers the definition and basic properties of continuous functions.
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 contiuous 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
\( IsContinuous(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
We 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 IsContinuous(\tau _1,\tau _2,g) \)
defines \( cl_1(A) \equiv Closure(A,\tau _1) \)
defines \( cl_2(A) \equiv 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 equavalence 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
Another 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 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 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 FinPow(B) \) have \( \{f^{-1}(W).\ W\in A\} \in 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 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 \)
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 \( IsContinuous(\tau _1 \text{ restricted to } A, \tau _2,restrict(f,A)) \)proof let \( g = 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 \( 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 = restrict(f,A) \) and A4: \( \tau _3 = \tau _1 \text{ restricted to } A \)
shows \( 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 \( IsContinuous(\tau _3, \tau _2, g) \) using restr_cont
ultimately have \( 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 \)
end
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) \)
Definition of IsContinuous:
\( IsContinuous(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
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 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 \)
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 \( A \subseteq \bigcup T \), \( 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 \)
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 FinPow(B)\} \text{ is a base for } T \)
lemma empty_open: assumes \( T \text{ is a topology } \) shows \( 0 \in T \)
lemma func1_1_L13: assumes \( f^{-1}(A) \neq 0 \) shows \( A\neq 0 \)
lemma inter_nempty_nempty: assumes \( \bigcap A \neq 0 \) shows \( A\neq 0 \)
lemma fin_image_fin: assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in FinPow(B) \) shows \( \{K(V).\ V\in N\} \in FinPow(C) \)
lemma (in topology0) fin_inter_open_open: assumes \( N\neq 0 \), \( N \in FinPow(T) \) shows \( \bigcap N \in T \)
Definition of FinPow:
\( FinPow(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma func1_1_L12: assumes \( B \subseteq Pow(Y) \) and \( B\neq 0 \) 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 func1_2_L1: assumes \( f:X\rightarrow Y \) and \( B\subseteq X \) shows \( 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 \( IsContinuous(\tau _1 \text{ restricted to } A, \tau _2,restrict(f,A)) \)
lemma (in two_top_spaces0) restr_image_cont: assumes \( f \text{ is continuous } \) shows \( IsContinuous(\tau _1, \tau _2 \text{ restricted to } f(X_1),f) \)
