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
\( \text{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 \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 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 \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 \)
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_defContinuous bijections that are open maps are homeomorphisms.
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_defInterior 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 \)
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 obvously 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_open2Pasting 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 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:
\( \text{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 \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 \)
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 \text{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 \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 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 } \)
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 homeo_open: assumes \( \text{IsAhomeomorphism}(T,S,f) \) and \( U\in T \) shows \( f(U) \in S \)
lemma inj_vimage_image: assumes \( f \in \text{inj}(X,Y) \) and \( A\subseteq X \) shows \( f^{-1}(f(A)) = A \)
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 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 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 TS \) shows \( \{x \in \bigcup T.\ \langle x,y\rangle \in V\} \in T \)
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 a Creative Commons Attribution 3.0 License. BTC: 1JzFajFtGwiKiRHbZyCB1KtASgsM1kFU2h