begin
This theory deals with the relations between continuous functions and convergence of filters. At the end of the file there some results about the building of functions in cartesian products.
Image filter
First of all, we will define the appropriate tools to work with functions and filters together.
We define the image filter as the collections of supersets of of images of sets from a filter.
definition
\( \mathfrak{F} \text{ is a filter on } X \Longrightarrow f:X\rightarrow Y \Longrightarrow f[\mathfrak{F} ].\ .\ Y \equiv \{A\in Pow(Y).\ \exists D\in \{f(B) .\ B\in \mathfrak{F} \}.\ D\subseteq A\} \)
Note that in the previous definition, it is necessary to state \(Y\) as the final set because \(f\) is also a function to every superset of its range. \(X\) can be changed by \( domain(f) \) without any change in the definition.
lemma base_image_filter:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( f:X\rightarrow Y \)
shows \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ Y) \) and \( (f[\mathfrak{F} ].\ .\ Y) \text{ is a filter on } Y \)proof{
}
assume \( 0 \in \{fB .\ B\in \mathfrak{F} \} \)
then obtain \( B \) where \( B\in \mathfrak{F} \) and f_B: \( fB=0 \)
then have \( B\in Pow(X) \) using assms(1), IsFilter_def
then have \( fB=\{fb.\ b\in B\} \) using image_fun, assms(2)
with f_B have \( \{fb.\ b\in B\}=0 \)
then have \( B=0 \)
with \( B\in \mathfrak{F} \) have \( False \) using IsFilter_def, assms(1)
then have \( 0\notin \{fB .\ B\in \mathfrak{F} \} \)
moreover
}
from assms(1) obtain \( S \) where \( S\in \mathfrak{F} \) using IsFilter_def
then have \( fS\in \{fB .\ B\in \mathfrak{F} \} \)
then have nA: \( \{fB .\ B\in \mathfrak{F} \}\neq 0 \)
moreover {
fix \( A \) \( B \)
assume \( A\in \{fB .\ B\in \mathfrak{F} \} \) and \( B\in \{fB .\ B\in \mathfrak{F} \} \)
then obtain \( AB \) \( BB \) where \( A=fAB \), \( B=fBB \), \( AB\in \mathfrak{F} \), \( BB\in \mathfrak{F} \)
then have \( A\cap B=(fAB)\cap (fBB) \)
then have I: \( f(AB\cap BB)\subseteq A\cap B \)
moreover
from assms(1), I, \( AB\in \mathfrak{F} \), \( BB\in \mathfrak{F} \) have \( AB\cap BB\in \mathfrak{F} \) using IsFilter_def
ultimately have \( \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D\subseteq A\cap B \)
then have \( \forall A\in \{fB .\ B\in \mathfrak{F} \}.\ \forall B\in \{fB .\ B\in \mathfrak{F} \}.\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D\subseteq A\cap B \)
ultimately have sbc: \( \{fB .\ B\in \mathfrak{F} \} \text{ satisfies the filter base condition } \) using SatisfiesFilterBase_def
moreover {
}
fix \( t \)
assume \( t\in \{fB .\ B\in \mathfrak{F} \} \)
then obtain \( B \) where \( B\in \mathfrak{F} \) and im_def: \( fB=t \)
with assms(1) have \( B\in Pow(X) \) unfolding IsFilter_def
with im_def, assms(2) have \( t=\{fx.\ x\in B\} \) using image_fun
with assms(2), \( B\in Pow(X) \) have \( t\subseteq Y \) using apply_funtype
then have nB: \( \{fB .\ B\in \mathfrak{F} \}\subseteq Pow(Y) \)
ultimately have \( ((\{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } \{A \in Pow(Y) .\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D \subseteq A\}) \wedge (\bigcup \{A \in Pow(Y) .\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D \subseteq A\}=Y)) \) using base_unique_filter_set2
then have \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } \{A \in Pow(Y) .\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D \subseteq A\} \)
with assms show \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ Y) \) using ImageFilter_def
moreover
}
qed
note sbc
moreover {
from nA obtain \( D \) where I: \( D\in \{fB .\ B\in \mathfrak{F} \} \)
moreover
from I, nB have \( D\subseteq Y \)
ultimately have \( Y\in \{A\in Pow(Y).\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D\subseteq A\} \)
then have \( \bigcup \{A\in Pow(Y).\ \exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D\subseteq A\}=Y \)
ultimately show \( (f[\mathfrak{F} ].\ .\ Y) \text{ is a filter on } Y \) using basic_filter, ImageFilter_def, assms
Continuous at a point vs. globally continuous
In this section we show that continuity of a function implies local continuity (at a point) and that local continuity at all points implies (global) continuity.
If a function is continuous, then it is continuous at every point.
lemma cont_global_imp_continuous_x:
assumes \( x\in \bigcup \tau _1 \), \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( f:(\bigcup \tau _1)\rightarrow (\bigcup \tau _2) \), \( x\in \bigcup \tau _1 \)
shows \( \forall U\in \tau _2.\ f(x)\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge f(V)\subseteq U) \)proof{
}
fix \( U \)
assume AS: \( U\in \tau _2 \), \( f(x)\in U \)
then have \( f^{-1}(U)\in \tau _1 \) using assms(2), IsContinuous_def
moreover
from assms(3) have \( f(f^{-1}(U))\subseteq U \) using function_image_vimage, fun_is_fun
moreover from assms(3), assms(4), AS(2) have \( x\in f^{-1}(U) \) using func1_1_L15
ultimately have \( \exists V\in \tau _1.\ x\in V \wedge fV\subseteq U \)
then show \( \forall U\in \tau _2.\ f(x)\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge f(V)\subseteq U) \)
qed
A function that is continuous at every point of its domain is continuous.
lemma ccontinuous_all_x_imp_cont_global:
assumes \( \forall x\in \bigcup \tau _1.\ \forall U\in \tau _2.\ fx\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge fV\subseteq U) \), \( f\in (\bigcup \tau _1)\rightarrow (\bigcup \tau _2) \) and \( \tau _1 \text{ is a topology } \)
shows \( \text{IsContinuous}(\tau _1,\tau _2,f) \)proof{
}
}
fix \( U \)
assume \( U\in \tau _2 \)
{
fix \( x \)
assume AS: \( x\in f^{-1}U \)
note \( U\in \tau _2 \)
moreover
from assms(2) have \( f ^{-1} U \subseteq \bigcup \tau _1 \) using func1_1_L6A
with AS have \( x\in \bigcup \tau _1 \)
with assms(1) have \( \forall U\in \tau _2.\ fx\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge fV\subseteq U) \)
moreover from AS, assms(2) have \( fx\in U \) using func1_1_L15
ultimately have \( \exists V\in \tau _1.\ x\in V \wedge fV\subseteq U \)
then obtain \( V \) where I: \( V\in \tau _1 \), \( x\in V \), \( f(V)\subseteq U \)
moreover
from I have \( V\subseteq \bigcup \tau _1 \)
moreover from assms(2), \( V\subseteq \bigcup \tau _1 \) have \( V\subseteq f^{-1}(fV) \) using func1_1_L9
ultimately have \( V \subseteq f^{-1}(U) \)
with \( V\in \tau _1 \), \( x\in V \) have \( \exists V\in \tau _1.\ x\in V \wedge V \subseteq f^{-1}(U) \)
hence \( \forall x\in f^{-1}(U).\ \exists V\in \tau _1.\ x\in V \wedge V\subseteq f^{-1}(U) \)
with assms(3) have \( f^{-1}(U) \in \tau _1 \) using open_neigh_open, topology0_def
hence \( \forall U\in \tau _2.\ f^{-1}U\in \tau _1 \)
then show \( thesis \) using IsContinuous_def
qed
Continuous functions and filters
In this section we consider the relations between filters and continuity.
If the function is continuous then if the filter converges to a point the image filter converges to the image point.
lemma (in two_top_spaces0) cont_imp_filter_conver_preserved:
assumes \( \mathfrak{F} \text{ is a filter on } X_1 \), \( f \text{ is continuous } \), \( \mathfrak{F} \rightarrow _F x\text{ in }\tau _1 \)
shows \( (f[\mathfrak{F} ].\ .\ X_2) \rightarrow _F (f(x))\text{ in }\tau _2 \)proof from assms(1), assms(3) have \( x\in X_1 \) using FilterConverges_def, topol_cntxs_valid(1), X1_def
have \( topology0(\tau _2) \) using topol_cntxs_valid(2)
moreover
qed
from assms(1) have \( (f[\mathfrak{F} ].\ .\ X_2) \text{ is a filter on } (\bigcup \tau _2) \) and \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ X_2) \) using base_image_filter, fmapAssum, X1_def, X2_def
moreover have \( \forall U\in Pow(\bigcup \tau _2).\ (fx)\in \text{Interior}(U,\tau _2) \longrightarrow (\exists D\in \{fB .\ B\in \mathfrak{F} \}.\ D\subseteq U) \)proof
moreover {
}
fix \( U \)
assume \( U\in Pow(X_2) \), \( (fx)\in \text{Interior}(U,\tau _2) \)
with \( x\in X_1 \) have xim: \( x\in f^{-1}( \text{Interior}(U,\tau _2)) \) and sub: \( f^{-1}( \text{Interior}(U,\tau _2))\in Pow(X_1) \) using func1_1_L6A, fmapAssum, func1_1_L15, fmapAssum
note sub
moreover
have \( \text{Interior}(U,\tau _2)\in \tau _2 \) using Top_2_L2, topol_cntxs_valid(2)
with assms(2) have \( f^{-1}( \text{Interior}(U,\tau _2))\in \tau _1 \) unfolding isContinuous_def, IsContinuous_def
with xim have \( x\in \text{Interior}(f^{-1}( \text{Interior}(U,\tau _2)),\tau _1) \) using Top_2_L3, topol_cntxs_valid(1)
moreover from assms(1), assms(3) have \( \{U\in Pow(X_1).\ x\in \text{Interior}(U,\tau _1)\}\subseteq \mathfrak{F} \) using FilterConverges_def, topol_cntxs_valid(1), X1_def
ultimately have \( f^{-1}( \text{Interior}(U,\tau _2))\in \mathfrak{F} \)
moreover
have \( f(f^{-1}( \text{Interior}(U,\tau _2)))\subseteq \text{Interior}(U,\tau _2) \) using function_image_vimage, fun_is_fun, fmapAssum
then have \( f(f^{-1}( \text{Interior}(U,\tau _2)))\subseteq U \) using Top_2_L1, topol_cntxs_valid(2)
ultimately have \( \exists D\in \{f(B) .\ B\in \mathfrak{F} \}.\ D\subseteq U \)
thus \( thesis \)
qed
from fmapAssum, \( x\in X_1 \) have \( f(x) \in X_2 \) by (rule apply_funtype )
hence \( f(x) \in \bigcup \tau _2 \)
ultimately show \( thesis \) by (rule convergence_filter_base2 )
Continuity in filter at every point of the domain implies global continuity.
lemma (in two_top_spaces0) filter_conver_preserved_imp_cont:
assumes \( \forall x\in \bigcup \tau _1.\ \forall \mathfrak{F} .\ ((\mathfrak{F} \text{ is a filter on } X_1) \wedge (\mathfrak{F} \rightarrow _F x\text{ in }\tau _1)) \longrightarrow ((f[\mathfrak{F} ].\ .\ X_2) \rightarrow _F (fx)\text{ in }\tau _2) \)
shows \( f\text{ is continuous } \)proof{
}
}
fix \( x \)
assume as2: \( x\in \bigcup \tau _1 \)
with assms have reg: \( \forall \mathfrak{F} .\ ((\mathfrak{F} \text{ is a filter on } X_1) \wedge (\mathfrak{F} \rightarrow _F x\text{ in }\tau _1)) \longrightarrow ((f[\mathfrak{F} ].\ .\ X_2) \rightarrow _F (fx)\text{ in }\tau _2) \)
let \( Neig = \{U \in Pow(\bigcup \tau _1) .\ x \in \text{Interior}(U, \tau _1)\} \)
from as2 have NFil: \( Neig\text{ is a filter on }X_1 \) and NCon: \( Neig \rightarrow _F x\text{ in }\tau _1 \) using topol_cntxs_valid(1), neigh_filter
{
fix \( U \)
assume \( U\in \tau _2 \), \( fx\in U \)
then have \( U\in Pow(\bigcup \tau _2) \), \( fx\in \text{Interior}(U,\tau _2) \) using topol_cntxs_valid(2), Top_2_L3
moreover
from NCon, NFil, reg have \( (f[Neig].\ .\ X_2) \rightarrow _F (fx)\text{ in }\tau _2 \)
moreover have \( (f[Neig].\ .\ X_2) \text{ is a filter on } X_2 \) using base_image_filter(2), NFil, fmapAssum
ultimately have \( U\in (f[Neig].\ .\ X_2) \) using FilterConverges_def, topol_cntxs_valid(2) unfolding X1_def, X2_def
moreover
from fmapAssum, NFil have \( \{fB .\ B\in Neig\} \text{ is a base filter } (f[Neig].\ .\ X_2) \) using base_image_filter(1), X1_def, X2_def
ultimately have \( \exists V\in \{fB .\ B\in Neig\}.\ V\subseteq U \) using basic_element_filter
then obtain \( B \) where \( B\in Neig \), \( fB\subseteq U \)
moreover
have \( \text{Interior}(B,\tau _1)\subseteq B \) using Top_2_L1, topol_cntxs_valid(1)
hence \( f \text{Interior}(B,\tau _1) \subseteq f(B) \)
moreover have \( \text{Interior}(B,\tau _1)\in \tau _1 \) using Top_2_L2, topol_cntxs_valid(1)
ultimately have \( \exists V\in \tau _1.\ x\in V \wedge fV\subseteq U \)
hence \( \forall U\in \tau _2.\ fx\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge fV\subseteq U) \)
hence \( \forall x\in \bigcup \tau _1.\ \forall U\in \tau _2.\ fx\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge fV\subseteq U) \)
then show \( thesis \) using ccontinuous_all_x_imp_cont_global, fmapAssum, X1_def, X2_def, isContinuous_def, tau1_is_top
qed
end
Definition of IsFilter:
\( \mathfrak{F} \text{ is a filter on } X \equiv (0\notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge \mathfrak{F} \subseteq Pow(X) \wedge \)
\( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)
Definition of SatisfiesFilterBase:
\( C \text{ satisfies the filter base condition } \equiv (\forall A\in C.\ \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B) \wedge C\neq 0 \wedge 0\notin C \)
theorem base_unique_filter_set2:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( ((C \text{ is a base filter } \mathfrak{F} ) \wedge \bigcup \mathfrak{F} =X) \longleftrightarrow \mathfrak{F} =\{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \)Definition of ImageFilter:
\( \mathfrak{F} \text{ is a filter on } X \Longrightarrow f:X\rightarrow Y \Longrightarrow f[\mathfrak{F} ].\ .\ Y \equiv \{A\in Pow(Y).\ \exists D\in \{f(B) .\ B\in \mathfrak{F} \}.\ D\subseteq A\} \)
theorem basic_filter:
assumes \( C \text{ is a base filter } \mathfrak{F} \)
shows \( (C \text{ satisfies the filter base condition }) \longleftrightarrow (\mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} ) \)Definition of IsContinuous:
\( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
lemma fun_is_fun:
assumes \( f:X\rightarrow Y \)
shows \( function(f) \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma func1_1_L6A:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A)\subseteq X \) lemma func1_1_L9:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( A \subseteq f^{-1}(f(A)) \) lemma (in topology0) open_neigh_open:
assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)
shows \( V\in T \)Definition of FilterConverges:
\( \mathfrak{F} \text{ is a filter on }\bigcup T \Longrightarrow \mathfrak{F} \rightarrow _Fx \equiv \)
\( x\in \bigcup T \wedge (\{U\in Pow(\bigcup T).\ x\in int(U)\} \subseteq \mathfrak{F} ) \)
lemma (in two_top_spaces0) topol_cntxs_valid: shows \( topology0(\tau _1) \) and \( topology0(\tau _2) \)
lemma (in two_top_spaces0) topol_cntxs_valid: shows \( topology0(\tau _1) \) and \( topology0(\tau _2) \)
lemma base_image_filter:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( f:X\rightarrow Y \)
shows \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ Y) \) and \( (f[\mathfrak{F} ].\ .\ Y) \text{ is a filter on } Y \) lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
lemma (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
theorem (in topology0) convergence_filter_base2:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \)
shows \( \mathfrak{F} \rightarrow _F x \) lemma (in topology0) neigh_filter:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
shows \( \text{Neigh} \text{ is a filter on }\bigcup T \) and \( \text{Neigh} \rightarrow _F x \) lemma base_image_filter:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( f:X\rightarrow Y \)
shows \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ Y) \) and \( (f[\mathfrak{F} ].\ .\ Y) \text{ is a filter on } Y \) lemma base_image_filter:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( f:X\rightarrow Y \)
shows \( \{fB .\ B\in \mathfrak{F} \} \text{ is a base filter } (f[\mathfrak{F} ].\ .\ Y) \) and \( (f[\mathfrak{F} ].\ .\ Y) \text{ is a filter on } Y \) lemma basic_element_filter:
assumes \( A\in \mathfrak{F} \) and \( C \text{ is a base filter } \mathfrak{F} \)
shows \( \exists D\in C.\ D\subseteq A \) lemma ccontinuous_all_x_imp_cont_global:
assumes \( \forall x\in \bigcup \tau _1.\ \forall U\in \tau _2.\ fx\in U \longrightarrow (\exists V\in \tau _1.\ x\in V \wedge fV\subseteq U) \), \( f\in (\bigcup \tau _1)\rightarrow (\bigcup \tau _2) \) and \( \tau _1 \text{ is a topology } \)
shows \( \text{IsContinuous}(\tau _1,\tau _2,f) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8