begin
The collection of all homeomorphisms of a topological space onto itself forms a group under composition. This file develops that group structure, connecting the theory of topological spaces with the algebraic theory of groups.
Group of homeomorphisms
We show that the homeomorphisms of a topological space onto itself form a group under composition, and compute this group for several concrete topologies.
First, we define the set of homeomorphisms.
definition
\( \text{HomeoG}(T) \equiv \{f:\bigcup T\rightarrow \bigcup T.\ \text{IsAhomeomorphism}(T,T,f)\} \)
The homeomorphisms are closed by composition.
lemma (in topology0) homeo_composition:
assumes \( f\in \text{HomeoG}(T) \), \( g\in \text{HomeoG}(T) \)
shows \( \text{Composition}(\bigcup T)\langle f, g\rangle \in \text{HomeoG}(T) \)proof from assms have fun: \( f\in \bigcup T\rightarrow \bigcup T \), \( g\in \bigcup T\rightarrow \bigcup T \) and homeo: \( \text{IsAhomeomorphism}(T,T,f) \), \( \text{IsAhomeomorphism}(T,T,g) \) unfolding HomeoG_def
from homeo have bij: \( f\in \text{bij}(\bigcup T,\bigcup T) \), \( g\in \text{bij}(\bigcup T,\bigcup T) \) and cont: \( \text{IsContinuous}(T,T,f) \), \( \text{IsContinuous}(T,T,g) \) and contconv: \( \text{IsContinuous}(T,T,converse(f)) \), \( \text{IsContinuous}(T,T,converse(g)) \) unfolding IsAhomeomorphism_def
from fun have \( f\circ g\in \bigcup T\rightarrow \bigcup T \) using comp_fun
moreover
qed
from bij have \( f\circ g\in \text{bij}(\bigcup T,\bigcup T) \) using comp_bij
moreover from cont have \( \text{IsContinuous}(T,T,f\circ g) \) using comp_cont
moreover have \( converse(f\circ g)=converse(g)\circ converse(f) \) using converse_comp
with contconv have \( \text{IsContinuous}(T,T,converse(f\circ g)) \) using comp_cont
ultimately have \( f\circ g\in \text{HomeoG}(T) \) unfolding HomeoG_def, IsAhomeomorphism_def
then show \( thesis \) using func_ZF_5_L2, fun
The identity function is a homeomorphism.
lemma (in topology0) homeo_id:
shows \( id(\bigcup T)\in \text{HomeoG}(T) \)proof have \( converse(id(\bigcup T))\circ id(\bigcup T)=id(\bigcup T) \) using left_comp_inverse, id_bij
then have \( converse(id(\bigcup T))=id(\bigcup T) \) using right_comp_id
then show \( thesis \) unfolding HomeoG_def, IsAhomeomorphism_def using id_cont, id_type, id_bij
qed
The homeomorphisms form a monoid and its neutral element is the identity.
theorem (in topology0) homeo_submonoid:
shows \( \text{IsAmonoid}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T))) \), \( \text{ TheNeutralElement}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T)))=id(\bigcup T) \)proof have cl: \( \text{HomeoG}(T) \text{ is closed under } \text{Composition}(\bigcup T) \) unfolding IsOpClosed_def using homeo_composition
moreover
have sub: \( \text{HomeoG}(T)\subseteq \bigcup T\rightarrow \bigcup T \) unfolding HomeoG_def
moreover have ne: \( \text{ TheNeutralElement}(\bigcup T\rightarrow \bigcup T, \text{Composition}(\bigcup T))\in \text{HomeoG}(T) \) using homeo_id, Group_ZF_2_5_L2(2)
ultimately show \( \text{IsAmonoid}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T))) \) using Group_ZF_2_5_L2(1), group0_1_T1 unfolding monoid0_def
from cl, sub, ne have \( \text{ TheNeutralElement}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T)))=\text{ TheNeutralElement}(\bigcup T\rightarrow \bigcup T, \text{Composition}(\bigcup T)) \) using Group_ZF_2_5_L2(1), group0_1_L6
moreover
qed
have \( id(\bigcup T)=\text{ TheNeutralElement}(\bigcup T\rightarrow \bigcup T, \text{Composition}(\bigcup T)) \) using Group_ZF_2_5_L2(2)
ultimately show \( \text{ TheNeutralElement}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T)))=id(\bigcup T) \)
The homeomorphisms form a group, with the composition.
theorem (in topology0) homeo_group:
shows \( \text{IsAgroup}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T))) \)proof{
}
fix \( x \)
assume AS: \( x\in \text{HomeoG}(T) \)
then have surj: \( x\in \text{surj}(\bigcup T,\bigcup T) \) and bij: \( x\in \text{bij}(\bigcup T,\bigcup T) \) unfolding HomeoG_def, IsAhomeomorphism_def, bij_def
from bij have \( converse(x)\in \text{bij}(\bigcup T,\bigcup T) \) using bij_converse_bij
with bij have conx_fun: \( converse(x)\in \bigcup T\rightarrow \bigcup T \), \( x\in \bigcup T\rightarrow \bigcup T \) unfolding bij_def, inj_def
from surj have id: \( x\circ converse(x)=id(\bigcup T) \) using right_comp_inverse
from conx_fun have \( \text{Composition}(\bigcup T)\langle x,converse(x)\rangle =x\circ converse(x) \) using func_ZF_5_L2
with id have \( \text{Composition}(\bigcup T)\langle x,converse(x)\rangle =id(\bigcup T) \)
moreover
have \( converse(x)\in \text{HomeoG}(T) \) using conx_fun(1), homeo_inv, AS unfolding HomeoG_def
ultimately have \( \exists M\in \text{HomeoG}(T).\ \text{Composition}(\bigcup T)\langle x,M\rangle =id(\bigcup T) \)
then have \( \forall x\in \text{HomeoG}(T).\ \exists M\in \text{HomeoG}(T).\ \text{Composition}(\bigcup T)\langle x,M\rangle =id(\bigcup T) \)
then show \( thesis \) using homeo_submonoid, definition_of_group
qed
Examples computed
We compute \(\text{HomeoG}\) for several concrete topologies: the cocardinal topology, the excluded set topology, the included set topology, and the order topology.
For the cocardinal topology every bijection is a homeomorphism, so \(\text{HomeoG}\) equals \(\text{bij}(X,X)\).
theorem homeo_cocardinal:
assumes \( \text{InfCard}(Q) \)
shows \( \text{HomeoG}(\text{CoCardinal}(X,Q))=\text{bij}(X,X) \)proof from assms have n: \( Q\neq 0 \) unfolding InfCard_def
then show \( \text{HomeoG}(\text{CoCardinal}(X,Q)) \subseteq \text{bij}(X, X) \) unfolding HomeoG_def, IsAhomeomorphism_def using union_cocardinal
{
fix \( f \)
assume a: \( f\in \text{bij}(X,X) \)
then have \( converse(f)\in \text{bij}(X,X) \) using bij_converse_bij
then have cinj: \( converse(f)\in \text{inj}(X,X) \) unfolding bij_def
from a have fun: \( f\in X\rightarrow X \) unfolding bij_def, inj_def
then have two: \( two\_top\_spaces0((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),f) \) unfolding two_top_spaces0_def using union_cocardinal, assms, n, CoCar_is_topology
{
fix \( N \)
assume \( N\text{ is closed in }(\text{CoCardinal}(X,Q)) \)
then have N_def: \( N=X \vee (N\in Pow(X) \wedge N\prec Q) \) using closed_sets_cocardinal, n
then have \( \text{restrict}(converse(f),N)\in \text{bij}(N,converse(f)N) \) using cinj, restrict_bij
then have \( N\approx f^{-1}N \) unfolding vimage_def, eqpoll_def
then have \( f^{-1}N\approx N \) using eqpoll_sym
with N_def have \( N=X \vee (f^{-1}N\prec Q \wedge N\in Pow(X)) \) using eq_lesspoll_trans
with fun have \( f^{-1}N=X \vee (f^{-1}N\prec Q \wedge (f^{-1}N)\in Pow(X)) \) using func1_1_L3, func1_1_L4
then have \( f^{-1}N \text{ is closed in }(\text{CoCardinal}(X,Q)) \) using closed_sets_cocardinal, n
then have \( \forall N.\ N\text{ is closed in }(\text{CoCardinal}(X,Q)) \longrightarrow f^{-1}N \text{ is closed in }(\text{CoCardinal}(X,Q)) \)
then have \( \text{IsContinuous}((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),f) \) using Top_ZF_2_1_L4, Top_ZF_2_1_L3, Top_ZF_2_1_L2, two
then have \( \forall f\in \text{bij}(X,X).\ \text{IsContinuous}((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),f) \)
then have \( \forall f\in \text{bij}(X,X).\ \text{IsContinuous}((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),f) \wedge \text{IsContinuous}((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),converse(f)) \) using bij_converse_bij
then have \( \forall f\in \text{bij}(X,X).\ \text{IsAhomeomorphism}((\text{CoCardinal}(X,Q)),(\text{CoCardinal}(X,Q)),f) \) unfolding IsAhomeomorphism_def using n, union_cocardinal
then show \( \text{bij}(X,X)\subseteq \text{HomeoG}((\text{CoCardinal}(X,Q))) \) unfolding HomeoG_def, bij_def, inj_def using n, union_cocardinal
qed
The homeomorphisms of the excluded set topology are exactly the bijections of \(X\) that map \(X\setminus T\) to itself.
theorem homeo_excluded:
assumes \( T \subseteq X \)
shows \( \text{HomeoG}(\text{ExcludedSet}(X,T))=\{f\in \text{bij}(X,X).\ f(X-T)=(X-T)\} \)proof have sub1: \( X-T\subseteq X \)
{
fix \( g \)
assume \( g\in \text{HomeoG}(\text{ExcludedSet}(X,T)) \)
then have fun: \( g:X\rightarrow X \) and bij: \( g\in \text{bij}(X,X) \) and hom: \( \text{IsAhomeomorphism}((\text{ExcludedSet}(X,T)),(\text{ExcludedSet}(X,T)),g) \) using union_excludedset unfolding IsAhomeomorphism_def, HomeoG_def
have op: \( X-T\in \text{ExcludedSet}(X,T) \) unfolding ExcludedSet_def
with hom have \( converse(g)^{-1}(X-T)\in \text{ExcludedSet}(X,T) \) unfolding IsAhomeomorphism_def, IsContinuous_def
then have \( converse(converse(g))(X-T)\in \text{ExcludedSet}(X,T) \) using vimage_def
with bij have D1: \( g(X-T)\in \text{ExcludedSet}(X,T) \) using converse_converse unfolding bij_def, inj_def, Pi_def, Sigma_def
from op, hom have D2: \( g^{-1}(X-T)\in \text{ExcludedSet}(X,T) \) unfolding IsAhomeomorphism_def, IsContinuous_def
{
assume as: \( g(X-T) = X \)
then have \( g^{-1}(g(X-T)) = g^{-1}X \)
then have \( converse(g)(g(X-T)) = g^{-1}X \) using vimage_def
then have \( (converse(g)\circ g)(X-T) = g^{-1}X \) using image_comp
then have \( id(X)(X-T) = g^{-1}X \) using left_comp_inverse, bij unfolding bij_def
moreover
have \( X-T \subseteq X \Longrightarrow id(X)(X-T) = X-T \)
ultimately have \( X-T = g^{-1}X \) using sub1
moreover
have \( converse(g):\text{bij}(X,X) \) using bij_converse_bij, bij
then have \( converse(g):\text{surj}(X,X) \) unfolding bij_def
then have \( converse(g)X = X \) using surj_range_image_domain
then have \( g^{-1}X =X \) using vimage_def
ultimately have \( X-T =X \)
with as have \( g(X-T) = X-T \)
moreover {
}
}
moreover
assume A: \( g(X-T)\in \{F \in Pow(X) .\ T \cap F = \emptyset \} \)
then have \( T\cap g(X-T) =0 \)
then have \( g(X-T) \subseteq X -T \) using A
then have \( g^{-1}(g(X-T)) \subseteq g^{-1}(X-T) \)
then have \( converse(g)(g(X-T)) \subseteq g^{-1}(X-T) \) using vimage_def
then have \( (converse(g)\circ g)(X-T) \subseteq g^{-1}(X-T) \) using image_comp
then have \( id(X)(X-T) \subseteq g^{-1}(X-T) \) using left_comp_inverse, bij unfolding bij_def
moreover
{
have \( X-T \subseteq X \Longrightarrow id(X)(X-T) = X-T \)
ultimately have C: \( X-T \subseteq g^{-1}(X-T) \) using sub1
assume as: \( g^{-1}(X-T) = X \)
then have \( g(g^{-1}(X-T)) = gX \)
then have \( g(converse(g)(X-T)) = gX \) using vimage_def
then have \( (g\circ converse(g))(X-T) = gX \) using image_comp
then have \( id(X)(X-T) = gX \) using right_comp_inverse, bij unfolding bij_def
moreover
have \( X-T \subseteq X \Longrightarrow id(X)(X-T) = X-T \)
ultimately have B: \( X-T = gX \) using sub1
moreover
from bij have \( gX = X \) using surj_range_image_domain unfolding bij_def
ultimately have \( X-T =X \)
with B have \( g(X-T) = X-T \)
moreover {
}
moreover
assume as: \( g^{-1}(X-T)\in \{F \in Pow(X) .\ T \cap F = \emptyset \} \)
then have \( T\cap g^{-1}(X-T) =0 \)
then have \( g^{-1}(X-T) \subseteq X -T \) using as
with C have \( g^{-1}(X-T) = X-T \)
then have \( g(g^{-1}(X-T)) = g(X-T) \)
then have \( g(converse(g)(X-T)) = g(X-T) \) using vimage_def
then have \( (g\circ converse(g))(X-T) = g(X-T) \) using image_comp
then have \( id(X)(X-T) = g(X-T) \) using right_comp_inverse, bij unfolding bij_def
moreover
have \( X-T \subseteq X \Longrightarrow id(X)(X-T) = X-T \)
ultimately have B: \( X-T = g(X-T) \) using sub1
then have \( g(X-T) = X-T \)
note D2
ultimately have \( g(X-T) = X-T \) unfolding ExcludedSet_def
note D1
ultimately have \( g(X-T) = X-T \) unfolding ExcludedSet_def
with bij have \( g\in \{f\in \text{bij}(X,X).\ f(X-T)=(X-T)\} \)
then show \( \text{HomeoG}(\text{ExcludedSet}(X,T))\subseteq \{f\in \text{bij}(X,X).\ f(X-T)=(X-T)\} \)
{
fix \( g \)
assume as: \( g\in \text{bij}(X,X) \), \( g(X-T)=X-T \)
then have inj: \( g\in \text{inj}(X,X) \) and im: \( g^{-1}(g(X-T))=g^{-1}(X-T) \) unfolding bij_def
from inj have \( g^{-1}(g(X-T))=X-T \) using inj_vimage_image, sub1
with im have as_3: \( g^{-1}(X-T)=X-T \)
{
fix \( A \)
assume \( A\in (\text{ExcludedSet}(X,T)) \)
then have \( A=X\vee A\cap T=0 \), \( A\subseteq X \) unfolding ExcludedSet_def
then have \( A\subseteq X-T\vee A=X \)
moreover {
}
moreover {
}
ultimately have \( gA\subseteq (X-T) \vee gA=X \)
assume \( A=X \)
with as(1) have \( gA=X \) using surj_range_image_domain unfolding bij_def
assume \( A\subseteq X-T \)
then have \( gA\subseteq g(X-T) \) using func1_1_L8
then have \( gA\subseteq (X-T) \) using as(2)
then have \( gA\in (\text{ExcludedSet}(X,T)) \) unfolding ExcludedSet_def
then have \( \forall A\in (\text{ExcludedSet}(X,T)).\ gA\in (\text{ExcludedSet}(X,T)) \)
moreover {
}
fix \( A \)
assume \( A\in (\text{ExcludedSet}(X,T)) \)
then have \( A=X\vee A\cap T=0 \), \( A\subseteq X \) unfolding ExcludedSet_def
then have \( A\subseteq X-T\vee A=X \)
moreover {
}
moreover {
}
ultimately have \( g^{-1}A\subseteq (X-T) \vee g^{-1}A=X \)
assume \( A=X \)
with as(1) have \( g^{-1}A=X \) using func1_1_L4 unfolding bij_def, inj_def
assume \( A\subseteq X-T \)
then have \( g^{-1}A\subseteq g^{-1}(X-T) \) using func1_1_L8
then have \( g^{-1}A\subseteq (X-T) \) using as_3
then have \( g^{-1}A\in (\text{ExcludedSet}(X,T)) \) unfolding ExcludedSet_def
then have \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),g) \) unfolding IsContinuous_def
moreover note as(1)
ultimately have \( \text{IsAhomeomorphism}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),g) \) using union_excludedset, bij_cont_open_homeo
with as(1) have \( g\in \text{HomeoG}(\text{ExcludedSet}(X,T)) \) unfolding bij_def, inj_def, HomeoG_def using union_excludedset
then show \( \{f \in \text{bij}(X, X) .\ f (X - T) = X - T\} \subseteq \text{HomeoG}(\text{ExcludedSet}(X,T)) \)
qed
Continuity in the included set topology implies continuity in the excluded set topology.
lemma cont_in_cont_ex:
assumes \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \), \( f:X\rightarrow X \), \( T\subseteq X \)
shows \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \)proof from assms(2,3) have two: \( two\_top\_spaces0(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) using union_includedset, includedset_is_topology unfolding two_top_spaces0_def
{
fix \( A \)
assume \( A\in (\text{ExcludedSet}(X,T)) \)
then have \( A\cap T=0 \vee A=X \), \( A\subseteq X \) unfolding ExcludedSet_def
then have \( A\text{ is closed in }(\text{IncludedSet}(X,T)) \) using closed_sets_includedset, assms
then have \( f^{-1}A\text{ is closed in }(\text{IncludedSet}(X,T)) \) using TopZF_2_1_L1, assms(1), two, assms, includedset_is_topology
then have \( (f^{-1}A)\cap T=0 \vee f^{-1}A=X \), \( f^{-1}A\subseteq X \) using closed_sets_includedset, assms(1,3)
then have \( f^{-1}A\in (\text{ExcludedSet}(X,T)) \) unfolding ExcludedSet_def
then show \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) unfolding IsContinuous_def
qed
Continuity in the excluded set topology implies continuity in the included set topology.
lemma cont_ex_cont_in:
assumes \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \), \( f:X\rightarrow X \), \( T\subseteq X \)
shows \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \)proof from assms(2) have two: \( two\_top\_spaces0(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) using union_excludedset, excludedset_is_topology unfolding two_top_spaces0_def
{
fix \( A \)
assume \( A\in (\text{IncludedSet}(X,T)) \)
then have \( T\subseteq A \vee A=0 \), \( A\subseteq X \) unfolding IncludedSet_def
then have \( A\text{ is closed in }(\text{ExcludedSet}(X,T)) \) using closed_sets_excludedset, assms
then have \( f^{-1}A\text{ is closed in }(\text{ExcludedSet}(X,T)) \) using TopZF_2_1_L1, assms(1), two, assms, excludedset_is_topology
then have \( T\subseteq (f^{-1}A) \vee f^{-1}A=0 \), \( f^{-1}A\subseteq X \) using closed_sets_excludedset, assms(1,3)
then have \( f^{-1}A\in (\text{IncludedSet}(X,T)) \) unfolding IncludedSet_def
then show \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) unfolding IsContinuous_def
qed
By the previous two lemmas, the homeomorphism groups of the included and excluded set topologies on \(X\) coincide.
lemma homeo_included:
assumes \( T\subseteq X \)
shows \( \text{HomeoG}(\text{IncludedSet}(X,T))=\{f \in \text{bij}(X, X) .\ f (X - T) = X - T\} \)proof{
}
fix \( f \)
assume \( f\in \text{HomeoG}(\text{IncludedSet}(X,T)) \)
then have hom: \( \text{IsAhomeomorphism}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) and fun: \( f\in X\rightarrow X \) and bij: \( f\in \text{bij}(X,X) \) unfolding HomeoG_def, IsAhomeomorphism_def using union_includedset, assms
then have cont: \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) unfolding IsAhomeomorphism_def
then have \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) using cont_in_cont_ex, fun, assms
moreover {
}
from hom have cont1: \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),converse(f)) \) unfolding IsAhomeomorphism_def
moreover
have \( converse(f):X\rightarrow X \) using bij_converse_bij, bij unfolding bij_def, inj_def
moreover note assms
ultimately have \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),converse(f)) \) using cont_in_cont_ex, assms
then have \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),converse(f)) \)
moreover note bij
ultimately have \( \text{IsAhomeomorphism}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) unfolding IsAhomeomorphism_def using union_excludedset
with fun have \( f\in \text{HomeoG}(\text{ExcludedSet}(X,T)) \) unfolding HomeoG_def using union_excludedset
then have \( \text{HomeoG}(\text{IncludedSet}(X,T))\subseteq \text{HomeoG}(\text{ExcludedSet}(X,T)) \)
moreover {
}
qed
fix \( f \)
assume \( f\in \text{HomeoG}(\text{ExcludedSet}(X,T)) \)
then have hom: \( \text{IsAhomeomorphism}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) and fun: \( f\in X\rightarrow X \) and bij: \( f\in \text{bij}(X,X) \) unfolding HomeoG_def, IsAhomeomorphism_def using union_excludedset, assms
then have cont: \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) unfolding IsAhomeomorphism_def
then have \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) using cont_ex_cont_in, fun, assms
moreover {
}
from hom have cont1: \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),converse(f)) \) unfolding IsAhomeomorphism_def
moreover
have \( converse(f):X\rightarrow X \) using bij_converse_bij, bij unfolding bij_def, inj_def
moreover note assms
ultimately have \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),converse(f)) \) using cont_ex_cont_in, assms
then have \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),converse(f)) \)
moreover note bij
ultimately have \( \text{IsAhomeomorphism}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) unfolding IsAhomeomorphism_def using union_includedset, assms
with fun have \( f\in \text{HomeoG}(\text{IncludedSet}(X,T)) \) unfolding HomeoG_def using union_includedset, assms
then have \( \text{HomeoG}(\text{ExcludedSet}(X,T))\subseteq \text{HomeoG}(\text{IncludedSet}(X,T)) \)
ultimately show \( thesis \) using homeo_excluded, assms
Every order isomorphism of a linearly ordered set is a homeomorphism of the induced order topology.
lemma homeo_order:
assumes \( \text{IsLinOrder}(X,r) \), \( \exists x y.\ x\neq y\wedge x\in X\wedge y\in X \)
shows \( ord\_iso(X,r,X,r)\subseteq \text{HomeoG}(OrdTopology X r) \)proof let \( \mathfrak{B} = \{ \text{IntervalX}(X, r, b, c) .\ \langle b,c\rangle \in X \times X\} \cup \{ \text{LeftRayX}(X, r, b) .\ b \in X\} \cup \)
\( \{ \text{RightRayX}(X, r, b) .\ b \in X\} \)
fix \( f \)
assume \( f\in ord\_iso(X,r,X,r) \)
then have bij: \( f\in \text{bij}(X,X) \) and ord: \( \forall x\in X.\ \forall y\in X.\ \langle x, y\rangle \in r \longleftrightarrow \langle f x, f y\rangle \in r \) unfolding ord_iso_def
have top: \( (OrdTopology X r)\text{ is a topology } \) using Ordtopology_is_a_topology(1), assms(1)
have union: \( \bigcup (OrdTopology X r) = X \) using union_ordtopology, assms
have twoSpac: \( two\_top\_spaces0(OrdTopology X r,OrdTopology X r,f) \) using bij, top, union unfolding two_top_spaces0_def, bij_def, inj_def
{
fix \( c \) \( d \)
assume A: \( c\in X \), \( d\in X \)
{
fix \( x \)
assume AA: \( x\in X \), \( x\neq c \), \( x\neq d \), \( \langle c,x\rangle \in r \), \( \langle x,d\rangle \in r \)
then have \( \langle fc,fx\rangle \in r \), \( \langle fx,fd\rangle \in r \) using A(2,1), ord
moreover {
}
assume \( fx=fc \vee fx=fd \)
with A(2,1), AA(1) have \( x=c\vee x=d \) using bij unfolding bij_def, inj_def
then have \( False \) using AA(2,3)
then have \( fx\neq fc \), \( fx\neq fd \)
moreover have \( fx\in X \) using bij, apply_type, AA(1) unfolding bij_def, inj_def
ultimately have \( fx\in \text{IntervalX}(X,r,fc,fd) \) unfolding IntervalX_def, Interval_def
then have \( \{fx.\ x\in \text{IntervalX}(X,r,c,d)\}\subseteq \text{IntervalX}(X,r,fc,fd) \) unfolding IntervalX_def, Interval_def
moreover {
}
}
ultimately have \( \{fx.\ x\in \text{IntervalX}(X,r,c,d)\}= \text{IntervalX}(X,r,fc,fd) \)
fix \( y \)
assume \( y\in \text{IntervalX}(X,r,fc,fd) \)
then have y: \( y\in X \), \( y\neq fc \), \( y\neq fd \), \( \langle fc,y\rangle \in r \), \( \langle y,fd\rangle \in r \) unfolding IntervalX_def, Interval_def
then obtain \( s \) where s: \( s\in X \), \( y=fs \) using bij unfolding bij_def, surj_def
{
assume \( s=c\vee s=d \)
then have \( fs=fc\vee fs=fd \)
then have \( False \) using s(2), y(2,3)
then have \( s\neq c \), \( s\neq d \)
moreover
have \( \langle c,s\rangle \in r \), \( \langle s,d\rangle \in r \) using y(4,5), s, ord, A(2,1)
moreover note s(1)
ultimately have \( s\in \text{IntervalX}(X,r,c,d) \) unfolding IntervalX_def, Interval_def
then have \( y\in \{fx.\ x\in \text{IntervalX}(X,r,c,d)\} \) using s(2)
moreover
have \( \text{IntervalX}(X,r,c,d)\subseteq X \) unfolding IntervalX_def
moreover have \( f:X\rightarrow X \) using bij unfolding bij_def, surj_def
ultimately have \( f \text{IntervalX}(X,r,c,d)= \text{IntervalX}(X,r,fc,fd) \) using func_imagedef
then have inter: \( \forall c\in X.\ \forall d\in X.\ f \text{IntervalX}(X,r,c,d)= \text{IntervalX}(X,r,fc,fd) \wedge fc\in X \wedge fd\in X \) using bij unfolding bij_def, inj_def
{
fix \( c \)
assume A: \( c\in X \)
{
fix \( x \)
assume AA: \( x\in X \), \( x\neq c \), \( \langle c,x\rangle \in r \)
then have \( \langle fc,fx\rangle \in r \) using A, ord
moreover {
}
assume \( fx=fc \)
with A, AA(1) have \( x=c \) using bij unfolding bij_def, inj_def
then have \( False \) using AA(2)
then have \( fx\neq fc \)
moreover have \( fx\in X \) using bij, apply_type, AA(1) unfolding bij_def, inj_def
ultimately have \( fx\in \text{RightRayX}(X,r,fc) \) unfolding RightRayX_def
then have \( \{fx.\ x\in \text{RightRayX}(X,r,c)\}\subseteq \text{RightRayX}(X,r,fc) \) unfolding RightRayX_def
moreover {
}
}
ultimately have \( \{fx.\ x\in \text{RightRayX}(X,r,c)\}= \text{RightRayX}(X,r,fc) \)
fix \( y \)
assume \( y\in \text{RightRayX}(X,r,fc) \)
then have y: \( y\in X \), \( y\neq fc \), \( \langle fc,y\rangle \in r \) unfolding RightRayX_def
then obtain \( s \) where s: \( s\in X \), \( y=fs \) using bij unfolding bij_def, surj_def
{
assume \( s=c \)
then have \( fs=fc \)
then have \( False \) using s(2), y(2)
then have \( s\neq c \)
moreover
have \( \langle c,s\rangle \in r \) using y(3), s, ord, A
moreover note s(1)
ultimately have \( s\in \text{RightRayX}(X,r,c) \) unfolding RightRayX_def
then have \( y\in \{fx.\ x\in \text{RightRayX}(X,r,c)\} \) using s(2)
moreover
have \( \text{RightRayX}(X,r,c)\subseteq X \) unfolding RightRayX_def
moreover have \( f:X\rightarrow X \) using bij unfolding bij_def, surj_def
ultimately have \( f \text{RightRayX}(X,r,c)= \text{RightRayX}(X,r,fc) \) using func_imagedef
then have rray: \( \forall c\in X.\ f \text{RightRayX}(X,r,c)= \text{RightRayX}(X,r,fc) \wedge fc\in X \) using bij unfolding bij_def, inj_def
{
fix \( c \)
assume A: \( c\in X \)
{
fix \( x \)
assume AA: \( x\in X \), \( x\neq c \), \( \langle x,c\rangle \in r \)
then have \( \langle fx,fc\rangle \in r \) using A, ord
moreover {
}
assume \( fx=fc \)
with A, AA(1) have \( x=c \) using bij unfolding bij_def, inj_def
then have \( False \) using AA(2)
then have \( fx\neq fc \)
moreover from AA(1) have \( fx\in X \) using bij, apply_type unfolding bij_def, inj_def
ultimately have \( fx\in \text{LeftRayX}(X,r,fc) \) unfolding LeftRayX_def
then have \( \{fx.\ x\in \text{LeftRayX}(X,r,c)\}\subseteq \text{LeftRayX}(X,r,fc) \) unfolding LeftRayX_def
moreover {
}
}
ultimately have \( \{fx.\ x\in \text{LeftRayX}(X,r,c)\}= \text{LeftRayX}(X,r,fc) \)
fix \( y \)
assume \( y\in \text{LeftRayX}(X,r,fc) \)
then have y: \( y\in X \), \( y\neq fc \), \( \langle y,fc\rangle \in r \) unfolding LeftRayX_def
then obtain \( s \) where s: \( s\in X \), \( y=fs \) using bij unfolding bij_def, surj_def
{
assume \( s=c \)
then have \( fs=fc \)
then have \( False \) using s(2), y(2)
then have \( s\neq c \)
moreover
have \( \langle s,c\rangle \in r \) using y(3), s, ord, A
moreover note s(1)
ultimately have \( s\in \text{LeftRayX}(X,r,c) \) unfolding LeftRayX_def
then have \( y\in \{fx.\ x\in \text{LeftRayX}(X,r,c)\} \) using s(2)
moreover
have \( \text{LeftRayX}(X,r,c)\subseteq X \) unfolding LeftRayX_def
moreover have \( f:X\rightarrow X \) using bij unfolding bij_def, surj_def
ultimately have \( f \text{LeftRayX}(X,r,c)= \text{LeftRayX}(X,r,fc) \) using func_imagedef
then have lray: \( \forall c\in X.\ f \text{LeftRayX}(X,r,c)= \text{LeftRayX}(X,r,fc)\wedge fc\in X \) using bij unfolding bij_def, inj_def
have r1: \( \forall U\in \mathfrak{B} .\ fU\in \mathfrak{B} \)proof
}
fix \( U \)
assume A: \( U\in \mathfrak{B} \)
{
assume \( U\in \{ \text{IntervalX}(X, r, b, c) .\ \langle b,c\rangle \in X \times X\} \)
with inter have \( fU\in \{ \text{IntervalX}(X, r, b, c) .\ \langle b,c\rangle \in X \times X\} \)
then have \( fU\in \mathfrak{B} \)
moreover {
}
moreover {
}
moreover
qed
assume \( U\in \{ \text{LeftRayX}(X, r, b) .\ b \in X\} \)
with lray have \( fU\in \{ \text{LeftRayX}(X, r, b) .\ b \in X\} \)
then have \( fU\in \mathfrak{B} \)
assume \( U\in \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
with rray have \( fU\in \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
then have \( fU\in \mathfrak{B} \)
note A
ultimately show \( fU\in \mathfrak{B} \)
from Ordtopology_is_a_topology(2), assms(1) have base: \( \mathfrak{B} \text{ is a base for }(OrdTopology X r) \)
then have r2: \( \mathfrak{B} \subseteq (OrdTopology X r) \) using base_sets_open
{
fix \( U \)
assume \( U\in \mathfrak{B} \)
with r1 have \( fU\in \mathfrak{B} \)
with r2 have \( fU\in (OrdTopology X r) \)
then have \( \forall U\in \mathfrak{B} .\ fU\in (OrdTopology X r) \)
moreover
{
from twoSpac have \( \bigwedge U.\ \mathfrak{B} \text{ is a base for } (OrdTopology X r) \Longrightarrow \)
\( \forall B\in \mathfrak{B} .\ f B \in (OrdTopology X r) \Longrightarrow \)
\( U \in (OrdTopology X r) \Longrightarrow f U \in (OrdTopology X r) \) using base_image_open
ultimately have f_open: \( \forall U\in (OrdTopology X r).\ fU\in (OrdTopology X r) \) using Ordtopology_is_a_topology(2), assms(1)
fix \( c \) \( d \)
assume A: \( c\in X \), \( d\in X \)
then obtain \( cc \) \( dd \) where pre: \( fcc=c \), \( fdd=d \), \( cc\in X \), \( dd\in X \) using bij unfolding bij_def, surj_def
with inter have \( f \text{IntervalX}(X, r, cc, dd) = \text{IntervalX}(X, r, c, d) \)
then have \( f^{-1}(f \text{IntervalX}(X, r, cc, dd)) = f^{-1}( \text{IntervalX}(X, r, c, d)) \)
moreover
have \( \text{IntervalX}(X, r, cc, dd)\subseteq X \) unfolding IntervalX_def
moreover have \( f\in \text{inj}(X,X) \) using bij unfolding bij_def
ultimately have \( \text{IntervalX}(X, r, cc, dd)=f^{-1} \text{IntervalX}(X, r, c, d) \) using inj_vimage_image
moreover
from pre(3,4) have \( \text{IntervalX}(X, r, cc, dd)\in \{ \text{IntervalX}(X,r,e1,e2).\ \langle e1,e2\rangle \in X\times X\} \)
then have \( \text{IntervalX}(X, r, cc, dd)\in \mathfrak{B} \)
with r2 have \( \text{IntervalX}(X, r, cc, dd)\in (OrdTopology X r) \)
ultimately have \( f^{-1} \text{IntervalX}(X, r, c, d)\in (OrdTopology X r) \)
then have inter: \( \forall c\in X.\ \forall d\in X.\ f^{-1} \text{IntervalX}(X, r, c, d)\in (OrdTopology X r) \)
{
fix \( c \)
assume A: \( c\in X \)
then obtain \( cc \) where pre: \( fcc=c \), \( cc\in X \) using bij unfolding bij_def, surj_def
with rray have \( f \text{RightRayX}(X, r, cc) = \text{RightRayX}(X, r, c) \)
then have \( f^{-1}(f \text{RightRayX}(X, r, cc)) = f^{-1}( \text{RightRayX}(X, r, c)) \)
moreover
have \( \text{RightRayX}(X, r, cc)\subseteq X \) unfolding RightRayX_def
moreover have \( f\in \text{inj}(X,X) \) using bij unfolding bij_def
ultimately have \( \text{RightRayX}(X, r, cc)=f^{-1} \text{RightRayX}(X, r, c) \) using inj_vimage_image
moreover
from pre(2) have \( \text{RightRayX}(X, r, cc)\in \{ \text{RightRayX}(X,r,e2).\ e2\in X\} \)
ultimately have \( f^{-1} \text{RightRayX}(X, r, c)\in (OrdTopology X r) \) using r2
then have rray: \( \forall c\in X.\ f^{-1} \text{RightRayX}(X, r, c)\in (OrdTopology X r) \)
{
fix \( c \)
assume A: \( c\in X \)
then obtain \( cc \) where pre: \( fcc=c \), \( cc\in X \) using bij unfolding bij_def, surj_def
with lray have \( f \text{LeftRayX}(X, r, cc) = \text{LeftRayX}(X, r, c) \)
then have \( f^{-1}(f \text{LeftRayX}(X, r, cc)) = f^{-1}( \text{LeftRayX}(X, r, c)) \)
moreover
have \( \text{LeftRayX}(X, r, cc)\subseteq X \) unfolding LeftRayX_def
moreover have \( f\in \text{inj}(X,X) \) using bij unfolding bij_def
ultimately have \( \text{LeftRayX}(X, r, cc)=f^{-1} \text{LeftRayX}(X, r, c) \) using inj_vimage_image
moreover
from pre(2) have \( \text{LeftRayX}(X, r, cc)\in \{ \text{LeftRayX}(X,r,e2).\ e2\in X\} \)
ultimately have \( f^{-1} \text{LeftRayX}(X, r, c)\in (OrdTopology X r) \) using r2
then have lray: \( \forall c\in X.\ f^{-1} \text{LeftRayX}(X, r, c)\in (OrdTopology X r) \)
{
fix \( U \)
assume \( U\in \{ \text{IntervalX}(X, r, b, c) .\ \langle b,c\rangle \in X \times X\} \cup \{ \text{LeftRayX}(X, r, b) .\ b \in X\} \cup \{ \text{RightRayX}(X, r, b) .\ b \in X\} \)
with lray, inter, rray have \( f^{-1}U\in (OrdTopology X r) \)
then have \( \forall U\in \{ \text{IntervalX}(X, r, b, c) .\ \langle b,c\rangle \in X \times X\} \cup \{ \text{LeftRayX}(X, r, b) .\ b \in X\} \cup \{ \text{RightRayX}(X, r, b) .\ b \in X\}.\ \)
\( f^{-1}U\in (OrdTopology X r) \)
from twoSpac, base, this have fcont: \( \text{IsContinuous}(OrdTopology X r,OrdTopology X r,f) \) by (rule Top_ZF_2_1_L5 )
from assms have \( \bigcup (OrdTopology X r) = X \) using union_ordtopology
with bij have b: \( f\in \text{bij}(\bigcup (OrdTopology X r),\bigcup (OrdTopology X r)) \)
from this, fcont, f_open have \( \text{IsAhomeomorphism}(OrdTopology X r,OrdTopology X r,f) \) by (rule bij_cont_open_homeo )
then show \( f\in \text{HomeoG}(OrdTopology X r) \) using b unfolding bij_def, inj_def, HomeoG_def
qed
Properties preserved by functions
Continuous surjections preserve connectedness and compactness. As consequences, quotient spaces of connected or compact spaces inherit those properties.
The continuous surjective image of a connected space is connected.
theorem (in two_top_spaces0) cont_image_conn:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( f\in \text{surj}(X_1,X_2) \), \( \tau _1\text{ is connected } \)
shows \( \tau _2\text{ is connected } \)proof{
}
fix \( U \)
assume Uop: \( U\in \tau _2 \) and Ucl: \( U\text{ is closed in }\tau _2 \)
from Uop, assms(1) have \( f^{-1}U\in \tau _1 \) unfolding IsContinuous_def
moreover
from Ucl, assms(1) have \( f^{-1}U\text{ is closed in }\tau _1 \) using TopZF_2_1_L1
ultimately have disj: \( f^{-1}U=0 \vee f^{-1}U=\bigcup \tau _1 \) using assms(3) unfolding IsConnected_def
moreover {
}
moreover {
}
ultimately have \( U=0\vee U=\bigcup \tau _2 \)
assume as: \( f^{-1}U\neq 0 \)
then have \( U\neq 0 \) using func1_1_L13
from as, disj have \( f^{-1}U=\bigcup \tau _1 \)
then have \( f(f^{-1}U)=f(\bigcup \tau _1) \)
moreover
have \( U\subseteq \bigcup \tau _2 \) using Uop
ultimately have \( U=f(\bigcup \tau _1) \) using surj_image_vimage, assms(2), Uop
then have \( \bigcup \tau _2=U \) using surj_range_image_domain, assms(2)
assume as: \( U\neq 0 \)
from Uop have s: \( U\subseteq \bigcup \tau _2 \)
with as obtain \( u \) where uU: \( u\in U \)
with s have \( u\in \bigcup \tau _2 \)
with assms(2) obtain \( w \) where \( fw=u \), \( w\in \bigcup \tau _1 \) unfolding surj_def, X1_def, X2_def
with uU have \( w\in f^{-1}U \) using func1_1_L15, assms(2) unfolding surj_def
then have \( f^{-1}U\neq 0 \)
then show \( thesis \) unfolding IsConnected_def
qed
A continuous function from a connected space to a totally-disconnected space must be constant.
corollary (in two_top_spaces0) cont_conn_tot_disc:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( \tau _1\text{ is connected } \), \( \tau _2\{is totally-disconnected\} \), \( f:X_1\rightarrow X_2 \), \( X_1\neq 0 \)
shows \( \exists q\in X_2.\ \forall w\in X_1.\ f(w)=q \)proof from assms(4) have surj: \( f\in \text{surj}(X_1,\text{range}(f)) \) using fun_is_surj
have sub: \( \text{range}(f)\subseteq X_2 \) using func1_1_L5B, assms(4)
from assms(1) have cont: \( \text{IsContinuous}(\tau _1,\tau _2\text{ restricted to }\text{range}(f),f) \) using restr_image_cont, range_image_domain, assms(4)
have union: \( \bigcup (\tau _2\text{ restricted to }\text{range}(f))=\text{range}(f) \) unfolding RestrictedTo_def using sub
then have \( two\_top\_spaces0(\tau _1,\tau _2\text{ restricted to }\text{range}(f),f) \) using surj, tau1_is_top, Top_1_L4, tau2_is_top unfolding two_top_spaces0_def, surj_def, topology0_def
then have conn: \( (\tau _2\text{ restricted to }\text{range}(f))\text{ is connected } \) using cont_image_conn, surj, assms(2), cont, union
then have \( \text{range}(f)\text{ is in the spectrum of }IsConnected \) using assms(3), sub, union unfolding IsTotDis_def, antiProperty_def
then have \( \text{range}(f)\preceq 1 \) using conn_spectrum
moreover
{
from assms(5) have \( fX_1\neq 0 \) using func1_1_L15A, assms(4)
then have \( \text{range}(f)\neq 0 \) using range_image_domain, assms(4)
ultimately obtain \( q \) where uniq: \( \text{range}(f)=\{q\} \) using lepoll_1_is_sing
fix \( w \)
assume \( w\in X_1 \)
then have \( fw\in \text{range}(f) \) using func1_1_L5A(2), assms(4)
with uniq have \( fw=q \)
then have \( \forall w\in X_1.\ fw=q \)
then show \( thesis \) using uniq, sub
qed
The continuous image of a compact space is compact.
theorem (in two_top_spaces0) cont_image_com:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( f\in \text{surj}(X_1,X_2) \), \( X_1\text{ is compact of cardinal }K\{in\}\tau _1 \)
shows \( X_2\text{ is compact of cardinal }K\{in\}\tau _2 \)proof have \( X_2\subseteq \bigcup \tau _2 \)
moreover {
}
}
qed
fix \( U \)
assume as: \( X_2\subseteq \bigcup U \), \( U\subseteq \tau _2 \)
then have P: \( \{f^{-1}V.\ V\in U\}\subseteq \tau _1 \) using assms(1) unfolding IsContinuous_def
from as(1) have \( f^{-1}X_2 \subseteq f^{-1}(\bigcup U) \)
then have \( f^{-1}X_2 \subseteq converse(f)(\bigcup U) \) unfolding vimage_def
moreover
have \( converse(f)(\bigcup U)=(\bigcup V\in U.\ converse(f)V) \) using image_UN
ultimately have \( f^{-1}X_2 \subseteq (\bigcup V\in U.\ converse(f)V) \)
then have \( f^{-1}X_2 \subseteq (\bigcup V\in U.\ f^{-1}V) \) unfolding vimage_def
then have \( X_1 \subseteq (\bigcup V\in U.\ f^{-1}V) \) using func1_1_L4, assms(2) unfolding surj_def
then have \( X_1 \subseteq \bigcup \{f^{-1}V.\ V\in U\} \)
with P, assms(3) have \( \exists N\in Pow(\{f^{-1}V.\ V\in U\}).\ X_1 \subseteq \bigcup N \wedge N\prec K \) unfolding IsCompactOfCard_def
then obtain \( N \) where N: \( N\in Pow(\{f^{-1}V.\ V\in U\}) \), \( X_1 \subseteq \bigcup N \), \( N\prec K \)
let \( FN = \{\langle R,fR\rangle .\ R\in N\} \)
have FN: \( FN:N\rightarrow \{fR.\ R\in N\} \) unfolding Pi_def, function_def, domain_def
{
fix \( S \)
assume \( S\in \{fR.\ R\in N\} \)
then obtain \( R \) where R_def: \( R\in N \), \( fR=S \)
then have \( \langle R,fR\rangle \in FN \)
then have \( FNR=fR \) using FN, apply_equality
then have \( \exists R\in N.\ FNR=S \) using R_def
then have surj: \( FN\in \text{surj}(N,\{fR.\ R\in N\}) \) unfolding surj_def using FN
from N have fin: \( N\prec K \) and sub: \( N\subseteq \{f^{-1}V.\ V\in U\} \) and cov: \( X_1 \subseteq \bigcup N \) unfolding FinPow_def
from sub have \( \{fR.\ R\in N\}\subseteq \{f(f^{-1}V).\ V\in U\} \)
moreover
have \( \forall V\in U.\ V\subseteq \bigcup \tau _2 \) using as(2)
ultimately have \( \{fR.\ R\in N\}\subseteq U \) using surj_image_vimage, assms(2)
moreover
from fin have N: \( N\preceq K \), \( Ord(K) \) using assms(3), lesspoll_imp_lepoll, Card_is_Ord unfolding IsCompactOfCard_def
then have \( \{fR.\ R\in N\}\preceq N \) using surj_fun_inv_2, surj
then have \( \{fR.\ R\in N\}\prec K \) using fin, lesspoll_trans1
moreover have \( \bigcup \{fR.\ R\in N\}=f(\bigcup N) \) using image_UN
then have \( fX_1 \subseteq \bigcup \{fR.\ R\in N\} \) using cov
then have \( X_2 \subseteq \bigcup \{fR.\ R\in N\} \) using assms(2), surj_range_image_domain
ultimately have \( \exists NN\in Pow(U).\ X_2 \subseteq \bigcup NN \wedge NN\prec K \)
then have \( \forall U\in Pow(\tau _2).\ X_2 \subseteq \bigcup U \longrightarrow (\exists NN\in Pow(U).\ X_2 \subseteq \bigcup NN \wedge NN\prec K) \)
ultimately show \( thesis \) using assms(3) unfolding IsCompactOfCard_def
Analogously to the connected case, the continuous image of a compact space in an anti-compact space is finite.
corollary (in two_top_spaces0) cont_comp_anti_comp:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( X_1\text{ is compact in }\tau _1 \), \( \tau _2\{is anti-compact\} \), \( f:X_1\rightarrow X_2 \), \( X_1\neq 0 \)
shows \( Finite(\text{range}(f)) \) and \( \text{range}(f)\neq 0 \)proof from assms(4) have surj: \( f\in \text{surj}(X_1,\text{range}(f)) \) using fun_is_surj
have sub: \( \text{range}(f)\subseteq X_2 \) using func1_1_L5B, assms(4)
from assms(1) have cont: \( \text{IsContinuous}(\tau _1,\tau _2\text{ restricted to }\text{range}(f),f) \) using restr_image_cont, range_image_domain, assms(4)
have union: \( \bigcup (\tau _2\text{ restricted to }\text{range}(f))=\text{range}(f) \) unfolding RestrictedTo_def using sub
then have \( two\_top\_spaces0(\tau _1,\tau _2\text{ restricted to }\text{range}(f),f) \) using surj, tau1_is_top, Top_1_L4, tau2_is_top unfolding surj_def, topology0_def, two_top_spaces0_def
then have \( \text{range}(f)\text{ is compact in }(\tau _2\text{ restricted to }\text{range}(f)) \) using surj, cont_image_com, cont, union, assms(2), Compact_is_card_nat
then have \( \text{range}(f)\text{ is in the spectrum of }(\lambda T.\ (\bigcup T) \text{ is compact in }T) \) using assms(3), sub, union unfolding IsAntiComp_def, antiProperty_def
then show \( Finite(\text{range}(f)) \) using compact_spectrum
from assms(5) have \( fX_1\neq 0 \) using func1_1_L15A, assms(4)
then show \( \text{range}(f)\neq 0 \) using range_image_domain, assms(4)
qed
A quotient of a compact space is compact.
corollary (in topology0) compQuot:
assumes \( (\bigcup T)\text{ is compact in }T \), \( \text{equiv}(\bigcup T,r) \)
shows \( (\bigcup T)//r\text{ is compact in }(\text{ quotient by }r) \)proof have surj: \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}\in \text{surj}(\bigcup T,(\bigcup T)//r) \) using quotient_proj_surj
moreover
have tot: \( \bigcup (\text{ quotient by }r)=(\bigcup T)//r \) using total_quo_equi, assms(2)
ultimately have cont: \( \text{IsContinuous}(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) using quotient_func_cont, EquivQuo_def, assms(2)
from surj, tot have \( two\_top\_spaces0(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) using topSpaceAssum, equiv_quo_is_top, assms(2) unfolding surj_def, two_top_spaces0_def
with surj, cont, tot, assms(1) show \( thesis \) using cont_image_com, Compact_is_card_nat
qed
A quotient of a connected space is connected.
corollary (in topology0) ConnQuot:
assumes \( T\text{ is connected } \), \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)\text{ is connected } \)proof have surj: \( \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}\in \text{surj}(\bigcup T,(\bigcup T)//r) \) using quotient_proj_surj
moreover
have tot: \( \bigcup (\text{ quotient by }r)=(\bigcup T)//r \) using total_quo_equi, assms(2)
ultimately have cont: \( \text{IsContinuous}(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) using quotient_func_cont, EquivQuo_def, assms(2)
from surj, tot have \( two\_top\_spaces0(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}) \) using topSpaceAssum, equiv_quo_is_top, assms(2) unfolding two_top_spaces0_def, surj_def
with surj, cont, tot, assms(1) show \( thesis \) using cont_image_conn
qed
end
Definition of HomeoG:
\( \text{HomeoG}(T) \equiv \{f:\bigcup T\rightarrow \bigcup T.\ \text{IsAhomeomorphism}(T,T,f)\} \)
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 comp_cont:
assumes \( \text{IsContinuous}(T,S,f) \) and \( \text{IsContinuous}(S,R,g) \)
shows \( \text{IsContinuous}(T,R,g\circ f) \) lemma func_ZF_5_L2:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,g\rangle = f\circ g \) lemma id_cont: shows \( \text{IsContinuous}(\tau ,\tau ,id(\bigcup \tau )) \)
Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in topology0) homeo_composition:
assumes \( f\in \text{HomeoG}(T) \), \( g\in \text{HomeoG}(T) \)
shows \( \text{Composition}(\bigcup T)\langle f, g\rangle \in \text{HomeoG}(T) \) lemma (in topology0) homeo_id: shows \( id(\bigcup T)\in \text{HomeoG}(T) \)
lemma Group_ZF_2_5_L2: shows \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \), \( id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X)) \)
lemma Group_ZF_2_5_L2: shows \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \), \( id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X)) \)
theorem (in monoid0) group0_1_T1:
assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \) lemma group0_1_L6:
assumes \( \text{IsAmonoid}(G,f) \) and \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) = \text{ TheNeutralElement}(G,f) \) lemma homeo_inv:
assumes \( \text{IsAhomeomorphism}(T,S,f) \)
shows \( \text{IsAhomeomorphism}(S,T,converse(f)) \) theorem (in topology0) homeo_submonoid: shows \( \text{IsAmonoid}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T))) \), \( \text{ TheNeutralElement}( \text{HomeoG}(T),\text{restrict}( \text{Composition}(\bigcup T), \text{HomeoG}(T)\times \text{HomeoG}(T)))=id(\bigcup T) \)
lemma definition_of_group:
assumes \( \text{IsAmonoid}(G,f) \) and \( \forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f) \)
shows \( \text{IsAgroup}(G,f) \) lemma union_cocardinal:
assumes \( T\neq 0 \)
shows \( \bigcup \text{CoCardinal}(X,T) = X \) lemma CoCar_is_topology:
assumes \( InfCard (Q) \)
shows \( \text{CoCardinal}(X,Q) \text{ is a topology } \) lemma closed_sets_cocardinal:
assumes \( T\neq 0 \)
shows \( D \text{ is closed in } \text{CoCardinal}(X,T) \longleftrightarrow (D\in Pow(X) \wedge D\prec T) \vee D=X \) 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 \) lemma (in two_top_spaces0) Top_ZF_2_1_L4:
assumes \( \forall B.\ ( B \subseteq X_2 \longrightarrow cl_1(f^{-1}(B)) \subseteq f^{-1}(cl_2(B)) ) \)
shows \( f \text{ is continuous } \) 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)) ) \) 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 union_excludedset: shows \( \bigcup \text{ExcludedSet}(X,T) = X \)
Definition of ExcludedSet:
\( \text{ExcludedSet}(X,U) \equiv \{F\in Pow(X).\ U \cap F=0\}\cup \{X\} \)
Definition of IsContinuous:
\( \text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1) \)
lemma surj_range_image_domain:
assumes \( f \in \text{surj}(A,B) \)
shows \( f(A) = B \) lemma inj_vimage_image:
assumes \( f \in \text{inj}(X,Y) \) and \( A\subseteq X \)
shows \( f^{-1}(f(A)) = A \) lemma func1_1_L8:
assumes \( A\subseteq B \)
shows \( f(A)\subseteq f(B) \) 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 union_includedset:
assumes \( T\subseteq X \)
shows \( \bigcup \text{IncludedSet}(X,T) = X \) theorem includedset_is_topology: shows \( \text{IncludedSet}(X,Q) \text{ is a topology } \)
lemma closed_sets_includedset:
assumes \( T\subseteq X \)
shows \( D \text{ is closed in } \text{IncludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (D \cap T)=0)\vee D=X \) 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 \) theorem excludedset_is_topology: shows \( \text{ExcludedSet}(X,Q) \text{ is a topology } \)
Definition of IncludedSet:
\( \text{IncludedSet}(X,U) \equiv \{F\in Pow(X).\ U \subseteq F\} \cup \{0\} \)
lemma closed_sets_excludedset: shows \( D \text{ is closed in }\text{ExcludedSet}(X,T) \longleftrightarrow (D\in Pow(X) \wedge (X \cap T) \subseteq D) \vee D=0 \)
lemma cont_in_cont_ex:
assumes \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \), \( f:X\rightarrow X \), \( T\subseteq X \)
shows \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \) lemma cont_ex_cont_in:
assumes \( \text{IsContinuous}(\text{ExcludedSet}(X,T),\text{ExcludedSet}(X,T),f) \), \( f:X\rightarrow X \), \( T\subseteq X \)
shows \( \text{IsContinuous}(\text{IncludedSet}(X,T),\text{IncludedSet}(X,T),f) \) theorem homeo_excluded:
assumes \( T \subseteq X \)
shows \( \text{HomeoG}(\text{ExcludedSet}(X,T))=\{f\in \text{bij}(X,X).\ f(X-T)=(X-T)\} \) theorem Ordtopology_is_a_topology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (OrdTopology X r) \text{ is a topology } \) and \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ is a base for } (OrdTopology X r) \) lemma union_ordtopology:
assumes \( \text{IsLinOrder}(X,r) \), \( \exists x y.\ x\neq y \wedge x\in X\wedge y\in X \)
shows \( \bigcup (OrdTopology X r)=X \)Definition of IntervalX:
\( \text{IntervalX}(X,r,b,c)\equiv ( \text{Interval}(r,b,c)\cap X)-\{b,c\} \)
Definition of Interval:
\( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \)Definition of RightRayX:
\( \text{RightRayX}(X,r,b)\equiv \{c\in X.\ \langle b,c\rangle \in r\}-\{b\} \)
Definition of LeftRayX:
\( \text{LeftRayX}(X,r,b)\equiv \{c\in X.\ \langle c,b\rangle \in r\}-\{b\} \)
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 \) theorem Ordtopology_is_a_topology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (OrdTopology X r) \text{ is a topology } \) and \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ is a base for } (OrdTopology X r) \) 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 IsConnected:
\( T \text{ is connected } \equiv \forall U.\ (U\in T \wedge (U \text{ is closed in }T)) \longrightarrow U=0\vee U=\bigcup T \)
lemma func1_1_L13:
assumes \( f^{-1}(A) \neq \emptyset \)
shows \( A\neq \emptyset \) lemma surj_image_vimage:
assumes \( f \in \text{surj}(X,Y) \) and \( A\subseteq Y \)
shows \( f(f^{-1}(A)) = A \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma func1_1_L5B:
assumes \( f:X\rightarrow Y \)
shows \( \text{range}(f) \subseteq Y \) 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 range_image_domain:
assumes \( f:X\rightarrow Y \)
shows \( f(X) = \text{range}(f) \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
theorem (in two_top_spaces0) cont_image_conn:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( f\in \text{surj}(X_1,X_2) \), \( \tau _1\text{ is connected } \)
shows \( \tau _2\text{ is connected } \)Definition of IsTotDis:
\( IsTotDis \equiv ANTI(IsConnected) \)
Definition of antiProperty:
\( T\{is anti-\}P \equiv \forall A\in Pow(\bigcup T).\ P(T\text{ restricted to }A) \longrightarrow (A \text{ is in the spectrum of } P) \)
lemma conn_spectrum: shows \( (A\text{ is in the spectrum of }IsConnected) \longleftrightarrow A\preceq 1 \)
lemma func1_1_L15A:
assumes \( f: X\rightarrow Y \) and \( A\subseteq X \) and \( A\neq \emptyset \)
shows \( f(A) \neq \emptyset \) lemma func1_1_L5A:
assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)
shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \)Definition of IsCompactOfCard:
\( K\text{ is compact of cardinal } Q\{in\}T \equiv (\text{Card}(Q) \wedge K \subseteq \bigcup T \wedge \)
\( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in Pow(M).\ K \subseteq \bigcup N \wedge N\prec Q))) \)
Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
theorem surj_fun_inv_2:
assumes \( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)
shows \( B\preceq A \) theorem (in two_top_spaces0) cont_image_com:
assumes \( \text{IsContinuous}(\tau _1,\tau _2,f) \), \( f\in \text{surj}(X_1,X_2) \), \( X_1\text{ is compact of cardinal }K\{in\}\tau _1 \)
shows \( X_2\text{ is compact of cardinal }K\{in\}\tau _2 \) lemma Compact_is_card_nat: shows \( K\text{ is compact in }T \longleftrightarrow (K\text{ is compact of cardinal } nat \{in\}T) \)
Definition of IsAntiComp:
\( T\{is anti-compact\} \equiv T\{is anti-\}(\lambda T.\ (\bigcup T)\text{ is compact in }T) \)
theorem compact_spectrum: shows \( (A \text{ is in the spectrum of } (\lambda T.\ (\bigcup T) \text{ is compact in }T)) \longleftrightarrow Finite(A) \)
lemma quotient_proj_surj: shows \( \{\langle b,r\{b\}\rangle .\ b\in A\}\in \text{surj}(A,A//r) \)
theorem (in topology0) total_quo_equi:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( \bigcup (\text{ quotient by }r)=(\bigcup T)//r \) lemma (in topology0) quotient_func_cont:
assumes \( f\in \text{surj}(\bigcup T,Y) \)
shows \( \text{IsContinuous}(T,(\text{ quotient topology in } Y\text{ by } f),f) \)Definition of EquivQuo:
\( \text{equiv}(\bigcup T,r)\Longrightarrow (\text{ quotient by } r) \equiv \text{ quotient topology in } (\bigcup T)//r\text{ by } \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\} \)
theorem (in topology0) equiv_quo_is_top:
assumes \( \text{equiv}(\bigcup T,r) \)
shows \( (\text{ quotient by }r)\text{ is a topology } \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
