imports TopologicalGroup_ZF Topology_ZF_properties_2

(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2013 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Topological groups 1› theory TopologicalGroup_ZF_1 imports TopologicalGroup_ZF Topology_ZF_properties_2 begin text{*This theory deals with some topological properties of topological groups.*} subsection{*Separation properties of topological groups*} text{*The topological groups have very specific properties. For instance, $G$ is @{text "T⇩_{0}"} iff it is @{text "T⇩_{3}"}.*} theorem(in topgroup) cl_point: assumes "x∈G" shows "cl({x}) = (⋂H∈𝒩⇩_{0}. x\<ltr>H)" proof- { have c:"cl({x}) = (⋂H∈𝒩⇩_{0}. {x}\<sad>H)" using cl_topgroup assms by auto { fix H assume "H∈𝒩⇩_{0}" then have "{x}\<sad>H=x\<ltr> H" using interval_add(3) assms by auto with `H∈𝒩⇩_{0}` have "{x}\<sad>H∈{x\<ltr>H. H∈𝒩⇩_{0}}" by auto } then have "{{x}\<sad>H. H∈𝒩⇩_{0}}⊆{x\<ltr>H. H∈𝒩⇩_{0}}" by auto moreover { fix H assume "H∈𝒩⇩_{0}" then have "{x}\<sad>H=x\<ltr> H" using interval_add(3) assms by auto with `H∈𝒩⇩_{0}` have "x\<ltr> H∈{{x}\<sad>H. H∈𝒩⇩_{0}}" by auto } then have "{x\<ltr>H. H∈𝒩⇩_{0}}⊆{{x}\<sad>H. H∈𝒩⇩_{0}}" by auto ultimately have "{{x}\<sad>H. H∈𝒩⇩_{0}}={x\<ltr>H. H∈𝒩⇩_{0}}" by auto then have "(⋂H∈𝒩⇩_{0}. {x}\<sad>H) = (⋂H∈𝒩⇩_{0}. x\<ltr>H)" by auto with c show "cl({x})=(⋂H∈𝒩⇩_{0}. x\<ltr>H)" by auto } qed text{*We prove the equivalence between $T_0$ and $T_1$ first.*} theorem (in topgroup) neu_closed_imp_T1: assumes "{𝟬}{is closed in}T" shows "T{is T⇩_{1}}" proof- { fix x z assume xG:"x∈G" and zG:"z∈G" and dis:"x≠z" then have clx:"cl({x})=(⋂H∈𝒩⇩_{0}. x\<ltr>H)" using cl_point by auto { fix y assume "y∈cl({x})" with clx have "y∈(⋂H∈𝒩⇩_{0}. x\<ltr>H)" by auto then have t:"∀H∈𝒩⇩_{0}. y∈x\<ltr>H" by auto from `y∈cl({x})` xG have yG:"y∈G" using Top_3_L11(1) G_def by auto { fix H assume HNeig:"H∈𝒩⇩_{0}" with t have "y∈x\<ltr>H" by auto then obtain n where "y=x\<ra>n" and "n∈H" unfolding ltrans_def grop_def LeftTranslation_def by auto with HNeig have nG:"n∈G" unfolding zerohoods_def by auto from `y=x\<ra>n` and `n∈H` have "(\<rm>x)\<ra>y∈H" using group0.group0_2_L18(2) group0_valid_in_tgroup xG nG yG unfolding grinv_def grop_def by auto } then have el:"(\<rm>x)\<ra>y∈(⋂𝒩⇩_{0})" using zneigh_not_empty by auto have "cl({𝟬})=(⋂H∈𝒩⇩_{0}. 𝟬\<ltr>H)" using cl_point zero_in_tgroup by auto moreover { fix H assume "H∈𝒩⇩_{0}" then have "H⊆G" unfolding zerohoods_def by auto then have "𝟬\<ltr>H=H" using image_id_same group0.trans_neutral(2) group0_valid_in_tgroup unfolding gzero_def ltrans_def by auto with `H∈𝒩⇩_{0}` have "𝟬\<ltr>H∈𝒩⇩_{0}" "H∈{𝟬\<ltr>H. H∈𝒩⇩_{0}}" by auto } then have "{𝟬\<ltr>H. H∈𝒩⇩_{0}}=𝒩⇩_{0}" by blast ultimately have "cl({𝟬})=(⋂𝒩⇩_{0})" by auto with el have "(\<rm>x)\<ra>y∈cl({𝟬})" by auto then have "(\<rm>x)\<ra>y∈{𝟬}" using assms Top_3_L8 G_def zero_in_tgroup by auto then have "(\<rm>x)\<ra>y=𝟬" by auto then have "y=\<rm>(\<rm>x)" using group0.group0_2_L9(2) group0_valid_in_tgroup neg_in_tgroup xG yG unfolding grop_def grinv_def by auto then have "y=x" using group0.group_inv_of_inv group0_valid_in_tgroup xG unfolding grinv_def by auto } then have "cl({x})⊆{x}" by auto then have "cl({x})={x}" using xG cl_contains_set G_def by blast then have "{x}{is closed in}T" using Top_3_L8 xG G_def by auto then have "(⋃T)-{x}∈T" using IsClosed_def by auto moreover from dis zG G_def have "z∈((⋃T)-{x}) ∧ x∉((⋃T)-{x})" by auto ultimately have "∃V∈T. z∈V∧x∉V" by(safe,auto) } then show "T{is T⇩_{1}}" using isT1_def by auto qed theorem (in topgroup) T0_imp_neu_closed: assumes "T{is T⇩_{0}}" shows "{𝟬}{is closed in}T" proof- { fix x assume "x∈cl({𝟬})" and "x≠𝟬" have "cl({𝟬})=(⋂H∈𝒩⇩_{0}. 𝟬\<ltr>H)" using cl_point zero_in_tgroup by auto moreover { fix H assume "H∈𝒩⇩_{0}" then have "H⊆G" unfolding zerohoods_def by auto then have "𝟬\<ltr>H=H" using image_id_same group0.trans_neutral(2) group0_valid_in_tgroup unfolding gzero_def ltrans_def by auto with `H∈𝒩⇩_{0}` have "𝟬\<ltr>H∈𝒩⇩_{0}" "H∈{𝟬\<ltr>H. H∈𝒩⇩_{0}}" by auto } then have "{𝟬\<ltr>H. H∈𝒩⇩_{0}}=𝒩⇩_{0}" by blast ultimately have "cl({𝟬})=(⋂𝒩⇩_{0})" by auto from `x≠𝟬` and `x∈cl({𝟬})` obtain U where "U∈T" and "(x∉U∧𝟬∈U)∨(𝟬∉U∧x∈U)" using assms Top_3_L11(1) zero_in_tgroup unfolding isT0_def G_def by blast moreover { assume "𝟬∈U" with `U∈T` have "U∈𝒩⇩_{0}" using zerohoods_def G_def Top_2_L3 by auto with `x∈cl({𝟬})` and `cl({𝟬})=(⋂𝒩⇩_{0})` have "x∈U" by auto } ultimately have "𝟬∉U" and "x∈U" by auto with `U∈T` `x∈cl({𝟬})` have "False" using cl_inter_neigh zero_in_tgroup unfolding G_def by blast } then have "cl({𝟬})⊆{𝟬}" by auto then have "cl({𝟬})={𝟬}" using zero_in_tgroup cl_contains_set G_def by blast then show ?thesis using Top_3_L8 zero_in_tgroup unfolding G_def by auto qed subsection{*Existence of nice neighbourhoods.*} theorem(in topgroup) exists_sym_zerohood: assumes "U∈𝒩⇩_{0}" shows "∃V∈𝒩⇩_{0}. (V⊆U∧ (\<sm>V)=V)" proof let ?V="U∩(\<sm>U)" have "U⊆G" using assms unfolding zerohoods_def by auto then have "?V⊆G" by auto have invg:" GroupInv(G, f) ∈ G → G" using group0_2_T2 Ggroup by auto have invb:"GroupInv(G, f) ∈bij(G,G)" using group0.group_inv_bij(2) group0_valid_in_tgroup by auto have "(\<sm>?V)=GroupInv(G,f)-``?V" unfolding setninv_def using group0.inv_image_vimage group0_valid_in_tgroup by auto also have "…=(GroupInv(G,f)-``U)∩(GroupInv(G,f)-``(\<sm>U))" using invim_inter_inter_invim invg by auto also have "…=(\<sm>U)∩(GroupInv(G,f)-``(GroupInv(G,f)``U))" unfolding setninv_def using group0.inv_image_vimage group0_valid_in_tgroup by auto also with `U⊆G` have "…=(\<sm>U)∩U" using inj_vimage_image invb unfolding bij_def by auto finally have "(\<sm>?V)=?V" by auto then show "?V ⊆ U ∧ (\<sm> ?V) = ?V" by auto from assms have "(\<sm>U)∈𝒩⇩_{0}" using neg_neigh_neigh by auto with assms have "𝟬∈int(U)∩int(\<sm>U)" unfolding zerohoods_def by auto moreover have "int(U)∩int(\<sm>U)∈T" using Top_2_L3 IsATopology_def topSpaceAssum Top_2_L4 by auto then have int:"int(int(U)∩int(\<sm>U))=int(U)∩int(\<sm>U)" using Top_2_L3 by auto have "int(U)∩int(\<sm>U)⊆?V" using Top_2_L1 by auto from interior_mono[OF this] int have "int(U)∩int(\<sm>U)⊆int(?V)" by auto ultimately have "𝟬∈int(?V)" by auto with `?V⊆G` show "?V∈𝒩⇩_{0}" using zerohoods_def by auto qed theorem(in topgroup) exists_procls_zerohood: assumes "U∈𝒩⇩_{0}" shows "∃V∈𝒩⇩_{0}. (V⊆U∧ (V\<sad>V)⊆U ∧ (\<sm>V)=V)" proof- have "int(U)∈T" using Top_2_L2 by auto then have "f-``(int(U))∈τ" using fcon IsContinuous_def by auto moreover have fne:"f ` ⟨𝟬, 𝟬⟩ = 𝟬" using group0.group0_2_L2 group0_valid_in_tgroup by auto have "𝟬∈int(U)" using assms unfolding zerohoods_def by auto then have "f -`` {𝟬}⊆f-``(int(U))" using func1_1_L8 vimage_def by auto then have "GroupInv(G,f)⊆f-``(int(U))" using group0.group0_2_T3 group0_valid_in_tgroup by auto then have "⟨𝟬,𝟬⟩∈f-``(int(U))" using fne zero_in_tgroup unfolding GroupInv_def by auto ultimately obtain W V where wop:"W∈T" and vop:"V∈T" and cartsub:"W×V⊆f-``(int(U))" and zerhood:"⟨𝟬,𝟬⟩∈W×V" using prod_top_point_neighb topSpaceAssum unfolding prodtop_def by force then have "𝟬∈W" and "𝟬∈V" by auto then have "𝟬∈W∩V" by auto have sub:"W∩V⊆G" using wop vop G_def by auto have assoc:"f∈G×G→G" using group0.group_oper_assocA group0_valid_in_tgroup by auto { fix t s assume "t∈W∩V" and "s∈W∩V" then have "t∈W" and "s∈V" by auto then have "⟨t,s⟩∈W×V" by auto then have "⟨t,s⟩∈f-``(int(U))" using cartsub by auto then have "f`⟨t,s⟩∈int(U)" using func1_1_L15 assoc by auto } then have "{f`⟨t,s⟩. ⟨t,s⟩∈(W∩V)×(W∩V)}⊆int(U)" by auto then have "(W∩V)\<sad>(W∩V)⊆int(U)" unfolding setadd_def using lift_subsets_explained(4) assoc sub by auto then have "(W∩V)\<sad>(W∩V)⊆U" using Top_2_L1 by auto from topSpaceAssum have "W∩V∈T" using vop wop unfolding IsATopology_def by auto then have "int(W∩V)=W∩V" using Top_2_L3 by auto with sub `𝟬∈W∩V` have "W∩V∈𝒩⇩_{0}" unfolding zerohoods_def by auto then obtain Q where "Q∈𝒩⇩_{0}" and "Q⊆W∩V" and "(\<sm>Q)=Q" using exists_sym_zerohood by blast then have "Q×Q⊆(W∩V)×(W∩V)" by auto moreover from `Q⊆W∩V` have "W∩V⊆G" and "Q⊆G" using vop wop unfolding G_def by auto ultimately have "Q\<sad>Q⊆(W∩V)\<sad>(W∩V)" using interval_add(2) func1_1_L8 by auto with `(W∩V)\<sad>(W∩V)⊆U` have "Q\<sad>Q⊆U" by auto from `Q∈𝒩⇩_{0}` have "𝟬∈Q" unfolding zerohoods_def using Top_2_L1 by auto with `Q\<sad>Q⊆U` `Q⊆G` have "𝟬\<ltr>Q⊆U" using interval_add(3) by auto with `Q⊆G` have "Q⊆U" unfolding ltrans_def using group0.trans_neutral(2) group0_valid_in_tgroup unfolding gzero_def using image_id_same by auto with `Q∈𝒩⇩_{0}` `Q\<sad>Q⊆U` `(\<sm>Q)=Q` show ?thesis by auto qed lemma (in topgroup) exist_basehoods_closed: assumes "U∈𝒩⇩_{0}" shows "∃V∈𝒩⇩_{0}. cl(V)⊆U" proof- from assms obtain V where "V∈𝒩⇩_{0}" "V⊆U" "(V\<sad>V)⊆U" "(\<sm>V)=V" using exists_procls_zerohood by blast have inv_fun:"GroupInv(G,f)∈G→G" using group0_2_T2 Ggroup by auto have f_fun:"f∈G×G→G" using group0.group_oper_assocA group0_valid_in_tgroup by auto { fix x assume "x∈cl(V)" with `V∈𝒩⇩_{0}` have "x∈⋃T" "V⊆⋃T" using Top_3_L11(1) unfolding zerohoods_def G_def by blast+ with `V∈𝒩⇩_{0}` have "x∈int(x\<ltr>V)" using elem_in_int_trans G_def by auto with `V⊆⋃T``x∈cl(V)` have "int(x\<ltr>V)∩V≠0" using cl_inter_neigh Top_2_L2 by blast then have "(x\<ltr>V)∩V≠0" using Top_2_L1 by blast then obtain q where "q∈(x\<ltr>V)" and "q∈V" by blast with `V⊆⋃T``x∈⋃T` obtain v where "q=x\<ra>v" "v∈V" unfolding ltrans_def grop_def using group0.ltrans_image group0_valid_in_tgroup unfolding G_def by auto from `V⊆⋃T` `v∈V``q∈V` have "v∈⋃T" "q∈⋃T" by auto with `q=x\<ra>v``x∈⋃T` have "q\<rs>v=x" using group0.group0_2_L18(1) group0_valid_in_tgroup unfolding G_def unfolding grsub_def grinv_def grop_def by auto moreover from `v∈V` have "(\<rm>v)∈(\<sm>V)" unfolding setninv_def grinv_def using func_imagedef inv_fun `V⊆⋃T` G_def by auto then have "(\<rm>v)∈V" using `(\<sm>V)=V` by auto with `q∈V` have "⟨q,\<rm>v⟩∈V×V" by auto then have "f`⟨q,\<rm>v⟩∈V\<sad>V" using lift_subset_suff f_fun `V⊆⋃T` unfolding setadd_def by auto with `V\<sad>V⊆U` have "q\<rs>v∈U" unfolding grsub_def grop_def by auto with `q\<rs>v=x` have "x∈U" by auto } then have "cl(V)⊆U" by auto with `V∈𝒩⇩_{0}` show ?thesis by auto qed subsection{*Rest of separation axioms*} theorem(in topgroup) T1_imp_T2: assumes "T{is T⇩_{1}}" shows "T{is T⇩_{2}}" proof- { fix x y assume ass:"x∈⋃T" "y∈⋃T" "x≠y" { assume "(\<rm>y)\<ra>x=𝟬" with ass(1,2) have "y=x" using group0.group0_2_L11[where a="y" and b="x"] group0_valid_in_tgroup by auto (*cannot be erased.*) with ass(3) have "False" by auto } then have "(\<rm>y)\<ra>x≠𝟬" by auto then have "𝟬≠(\<rm>y)\<ra>x" by auto from `y∈⋃T` have "(\<rm>y)∈⋃T" using neg_in_tgroup G_def by auto with `x∈⋃T` have "(\<rm>y)\<ra>x∈⋃T" using group0.group_op_closed[where a="\<rm>y" and b="x"] group0_valid_in_tgroup unfolding (*cannot be erased.*) G_def by auto with assms `𝟬≠(\<rm>y)\<ra>x` obtain U where "U∈T" and "(\<rm>y)\<ra>x∉U" and "𝟬∈U" unfolding isT1_def using zero_in_tgroup by auto then have "U∈𝒩⇩_{0}" unfolding zerohoods_def G_def using Top_2_L3 by auto then obtain Q where "Q∈𝒩⇩_{0}" "Q⊆U" "(Q\<sad>Q)⊆U" "(\<sm>Q)=Q" using exists_procls_zerohood by blast with `(\<rm>y)\<ra>x∉U` have "(\<rm>y)\<ra>x∉Q" by auto from `Q∈𝒩⇩_{0}` have "Q⊆G" unfolding zerohoods_def by auto { assume "x∈y\<ltr>Q" with `Q⊆G` `y∈⋃T` obtain u where "u∈Q" and "x=y\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image group0_valid_in_tgroup unfolding G_def by auto with `Q⊆G` have "u∈⋃T" unfolding G_def by auto with `x=y\<ra>u` `y∈⋃T` `x∈⋃T` `Q⊆G` have "(\<rm>y)\<ra>x=u" using group0.group0_2_L18(2) group0_valid_in_tgroup unfolding G_def unfolding grsub_def grinv_def grop_def by auto with `u∈Q` have "(\<rm>y)\<ra>x∈Q" by auto then have "False" using `(\<rm>y)\<ra>x∉Q` by auto } then have "x∉y\<ltr>Q" by auto moreover { assume "y∈x\<ltr>Q" with `Q⊆G` `x∈⋃T` obtain u where "u∈Q" and "y=x\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image group0_valid_in_tgroup unfolding G_def by auto with `Q⊆G` have "u∈⋃T" unfolding G_def by auto with `y=x\<ra>u` `y∈⋃T` `x∈⋃T` `Q⊆G` have "(\<rm>x)\<ra>y=u" using group0.group0_2_L18(2) group0_valid_in_tgroup unfolding G_def unfolding grsub_def grinv_def grop_def by auto with `u∈Q` have "(\<rm>y)\<ra>x=\<rm>u" using group0.group_inv_of_two[OF group0_valid_in_tgroup group0.inverse_in_group[OF group0_valid_in_tgroup,of x],of y] (*From here no checked*) using `x∈⋃T` `y∈⋃T` using group0.group_inv_of_inv[OF group0_valid_in_tgroup] unfolding G_def grinv_def grop_def by auto moreover from `u∈Q` have "(\<rm>u)∈(\<sm>Q)" unfolding setninv_def grinv_def using func_imagedef[OF group0_2_T2[OF Ggroup] `Q⊆G`] by auto ultimately have "(\<rm>y)\<ra>x∈Q" using `(\<rm>y)\<ra>x∉Q` `(\<sm>Q)=Q` unfolding setninv_def grinv_def by auto then have "False" using `(\<rm>y)\<ra>x∉Q` by auto } then have "y∉x\<ltr>Q" by auto moreover { fix t assume "t∈(x\<ltr>Q)∩(y\<ltr>Q)" then have "t∈(x\<ltr>Q)" "t∈(y\<ltr>Q)" by auto with `Q⊆G` `x∈⋃T` `y∈⋃T` obtain u v where "u∈Q" "v∈Q" and "t=x\<ra>u" "t=y\<ra>v" unfolding ltrans_def grop_def using group0.ltrans_image[OF group0_valid_in_tgroup] unfolding G_def by auto then have "x\<ra>u=y\<ra>v" by auto moreover from `u∈Q` `v∈Q` `Q⊆G` have "u∈⋃T" "v∈⋃T" unfolding G_def by auto moreover note `x∈⋃T` `y∈⋃T` ultimately have "(\<rm>y)\<ra>(x\<ra>u)=v" using group0.group0_2_L18(2)[OF group0_valid_in_tgroup, of y v "x\<ra>u"] group0.group_op_closed[OF group0_valid_in_tgroup, of x u] unfolding G_def unfolding grsub_def grinv_def grop_def by auto then have "((\<rm>y)\<ra>x)\<ra>u=v" using group0.group_oper_assoc[OF group0_valid_in_tgroup] unfolding grop_def using `x∈⋃T` `y∈⋃T` `u∈⋃T` using group0.inverse_in_group[OF group0_valid_in_tgroup] unfolding G_def by auto then have "((\<rm>y)\<ra>x)=v\<rs>u" using group0.group0_2_L18(1)[OF group0_valid_in_tgroup,of "(\<rm>y)\<ra>x" u v] using `(\<rm>y)\<ra>x∈⋃T` `u∈⋃T` `v∈⋃T` unfolding G_def grsub_def grinv_def grop_def by force moreover from `u∈Q` have "(\<rm>u)∈(\<sm>Q)" unfolding setninv_def grinv_def using func_imagedef[OF group0_2_T2[OF Ggroup] `Q⊆G`] by auto then have "(\<rm>u)∈Q" using `(\<sm>Q)=Q` by auto with `v∈Q` have "⟨v,\<rm>u⟩∈Q×Q" by auto then have "f`⟨v,\<rm>u⟩∈Q\<sad>Q" using lift_subset_suff[OF group0.group_oper_assocA[OF group0_valid_in_tgroup] `Q⊆G` `Q⊆G`] unfolding setadd_def by auto with `Q\<sad>Q⊆U` have "v\<rs>u∈U" unfolding grsub_def grop_def by auto ultimately have "(\<rm>y)\<ra>x∈U" by auto with `(\<rm>y)\<ra>x∉U` have "False" by auto } then have "(x\<ltr>Q)∩(y\<ltr>Q)=0" by auto moreover have "x∈int(x\<ltr>Q)""y∈int(y\<ltr>Q)" using elem_in_int_trans `Q∈𝒩⇩_{0}` `x∈⋃T` `y∈⋃T` unfolding G_def by auto moreover have "int(x\<ltr>Q)⊆(x\<ltr>Q)""int(y\<ltr>Q)⊆(y\<ltr>Q)" using Top_2_L1 by auto moreover have "int(x\<ltr>Q)∈T" "int(y\<ltr>Q)∈T" using Top_2_L2 by auto ultimately have "int(x\<ltr>Q)∈T ∧ int(y\<ltr>Q)∈T ∧ x ∈ int(x\<ltr>Q) ∧ y ∈ int(y\<ltr>Q) ∧ int(x\<ltr>Q) ∩ int(y\<ltr>Q) = 0" by blast then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" by auto } then show ?thesis using isT2_def by auto qed text{*Here follow some auxiliary lemmas.*} lemma (in topgroup) trans_closure: assumes "x∈G" "A⊆G" shows "cl(x\<ltr>A)=x\<ltr>cl(A)" proof- have "⋃T-(⋃T-(x\<ltr>A))=(x\<ltr>A)" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup assms(1)] unfolding image_def range_def domain_def converse_def Pi_def by auto then have "cl(x\<ltr>A)=⋃T-int(⋃T-(x\<ltr>A))" using Top_3_L11(2)[of "⋃T-(x\<ltr>A)"] by auto moreover have "x\<ltr>G=G" using surj_image_eq group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] bij_def by auto then have "⋃T-(x\<ltr>A)=x\<ltr>(⋃T-A)" using inj_image_dif[of "LeftTranslation(G, f, x)""G""G", OF _ assms(2)] unfolding ltrans_def G_def using group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] bij_def by auto then have "int(⋃T-(x\<ltr>A))=int(x\<ltr>(⋃T-A))" by auto then have "int(⋃T-(x\<ltr>A))=x\<ltr>int(⋃T-A)" using trans_interior[OF assms(1),of "⋃T-A"] unfolding G_def by force have "⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))" using Top_3_L11(2)[of "⋃T-A"] by force have "⋃T-(⋃T-A)=A" using assms(2) G_def by auto with `⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))` have "⋃T-int(⋃T-A)=cl(A)" by auto have "⋃T-(⋃T-int(⋃T-A))=int(⋃T-A)" using Top_2_L2 by auto with `⋃T-int(⋃T-A)=cl(A)` have "int(⋃T-A)=⋃T-cl(A)" by auto with `int(⋃T-(x\<ltr>A))=x\<ltr>int(⋃T-A)` have "int(⋃T-(x\<ltr>A))=x\<ltr>(⋃T-cl(A))" by auto with `x\<ltr>G=G` have "int(⋃T-(x\<ltr>A))=⋃T-(x\<ltr>cl(A))" using inj_image_dif[of "LeftTranslation(G, f, x)""G""G""cl(A)"] unfolding ltrans_def using group0.trans_bij(2)[OF group0_valid_in_tgroup assms(1)] Top_3_L11(1) assms(2) unfolding bij_def G_def by auto then have "⋃T-int(⋃T-(x\<ltr>A))=⋃T-(⋃T-(x\<ltr>cl(A)))" by auto then have "⋃T-int(⋃T-(x\<ltr>A))=x\<ltr>cl(A)" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup assms(1)] unfolding image_def range_def domain_def converse_def Pi_def by auto with `cl(x\<ltr>A)=⋃T-int(⋃T-(x\<ltr>A))` show ?thesis by auto qed lemma (in topgroup) trans_interior2: assumes A1: "g∈G" and A2: "A⊆G" shows "int(A)\<rtr>g = int(A\<rtr>g)" proof - from assms have "A ⊆ ⋃T" and "IsAhomeomorphism(T,T,RightTranslation(G,f,g))" using tr_homeo by auto then show ?thesis using int_top_invariant by simp qed lemma (in topgroup) trans_closure2: assumes "x∈G" "A⊆G" shows "cl(A\<rtr>x)=cl(A)\<rtr>x" proof- have "⋃T-(⋃T-(A\<rtr>x))=(A\<rtr>x)" unfolding ltrans_def using group0.group0_5_L1(1)[OF group0_valid_in_tgroup assms(1)] unfolding image_def range_def domain_def converse_def Pi_def by auto then have "cl(A\<rtr>x)=⋃T-int(⋃T-(A\<rtr>x))" using Top_3_L11(2)[of "⋃T-(A\<rtr>x)"] by auto moreover have "G\<rtr>x=G" using surj_image_eq group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] bij_def by auto then have "⋃T-(A\<rtr>x)=(⋃T-A)\<rtr>x" using inj_image_dif[of "RightTranslation(G, f, x)""G""G", OF _ assms(2)] unfolding rtrans_def G_def using group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] bij_def by auto then have "int(⋃T-(A\<rtr>x))=int((⋃T-A)\<rtr>x)" by auto then have "int(⋃T-(A\<rtr>x))=int(⋃T-A)\<rtr>x" using trans_interior2[OF assms(1),of "⋃T-A"] unfolding G_def by force have "⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))" using Top_3_L11(2)[of "⋃T-A"] by force have "⋃T-(⋃T-A)=A" using assms(2) G_def by auto with `⋃T-int(⋃T-A)=cl(⋃T-(⋃T-A))` have "⋃T-int(⋃T-A)=cl(A)" by auto have "⋃T-(⋃T-int(⋃T-A))=int(⋃T-A)" using Top_2_L2 by auto with `⋃T-int(⋃T-A)=cl(A)` have "int(⋃T-A)=⋃T-cl(A)" by auto with `int(⋃T-(A\<rtr>x))=int(⋃T-A)\<rtr>x` have "int(⋃T-(A\<rtr>x))=(⋃T-cl(A))\<rtr>x" by auto with `G\<rtr>x=G` have "int(⋃T-(A\<rtr>x))=⋃T-(cl(A)\<rtr>x)" using inj_image_dif[of "RightTranslation(G, f, x)""G""G""cl(A)"] unfolding rtrans_def using group0.trans_bij(1)[OF group0_valid_in_tgroup assms(1)] Top_3_L11(1) assms(2) unfolding bij_def G_def by auto then have "⋃T-int(⋃T-(A\<rtr>x))=⋃T-(⋃T-(cl(A)\<rtr>x))" by auto then have "⋃T-int(⋃T-(A\<rtr>x))=cl(A)\<rtr>x" unfolding ltrans_def using group0.group0_5_L1(1)[OF group0_valid_in_tgroup assms(1)] unfolding image_def range_def domain_def converse_def Pi_def by auto with `cl(A\<rtr>x)=⋃T-int(⋃T-(A\<rtr>x))` show ?thesis by auto qed lemma (in topgroup) trans_subset: assumes "A⊆((\<rm>x)\<ltr>B)""x∈G""A⊆G""B⊆G" shows "x\<ltr>A⊆B" proof- { fix t assume "t∈x\<ltr>A" with `x∈G` `A⊆G` obtain u where "u∈A" "t=x\<ra>u" unfolding ltrans_def grop_def using group0.ltrans_image[OF group0_valid_in_tgroup] unfolding G_def by auto with `x∈G` `A⊆G` `u∈A` have "(\<rm>x)\<ra>t=u" using group0.group0_2_L18(2)[OF group0_valid_in_tgroup, of "x""u""t"] group0.group_op_closed[OF group0_valid_in_tgroup,of x u] unfolding grop_def grinv_def by auto with `u∈A` have "(\<rm>x)\<ra>t∈A" by auto with `A⊆(\<rm>x)\<ltr>B` have "(\<rm>x)\<ra>t∈(\<rm>x)\<ltr>B" by auto with `B⊆G` obtain v where "(\<rm>x)\<ra>t=(\<rm>x)\<ra>v" "v∈B" unfolding ltrans_def grop_def using neg_in_tgroup[OF `x∈G`] group0.ltrans_image[OF group0_valid_in_tgroup] unfolding G_def by auto have "LeftTranslation(G,f,\<rm>x)∈inj(G,G)" using group0.trans_bij(2)[OF group0_valid_in_tgroup neg_in_tgroup[OF `x∈G`]] bij_def by auto then have eq:"∀A∈G. ∀B∈G. LeftTranslation(G,f,\<rm>x)`A=LeftTranslation(G,f,\<rm>x)`B ⟶ A=B" unfolding inj_def by auto { fix A B assume "A∈G""B∈G" assume "f`⟨\<rm>x,A⟩=f`⟨\<rm>x,B⟩" then have "LeftTranslation(G,f,\<rm>x)`A=LeftTranslation(G,f,\<rm>x)`B" using group0.group0_5_L2(2)[OF group0_valid_in_tgroup neg_in_tgroup[OF `x∈G`]] `A∈G``B∈G` by auto with eq `A∈G``B∈G` have "A=B" by auto } then have eq1:"∀A∈G. ∀B∈G. f`⟨\<rm>x,A⟩=f`⟨\<rm>x,B⟩ ⟶ A=B" by auto from `A⊆G` `u∈A` have "u∈G" by auto with `v∈B` `B⊆G` `t=x\<ra>u` have "t∈G" "v∈G" using group0.group_op_closed[OF group0_valid_in_tgroup `x∈G`,of u] unfolding grop_def by auto with eq1 `(\<rm>x)\<ra>t=(\<rm>x)\<ra>v` have "t=v" unfolding grop_def by auto with `v∈B` have "t∈B" by auto } then show ?thesis by auto qed text{*Every topological group is regular, and hence $T_3$. The proof is in the next section, since it uses local properties.*} subsection{*Local properties*} text{*In a topological group, all local properties depend only on the neighbourhoods of the neutral element; when considering topological properties. The next result of regularity, will use this idea, since translations preserve closed sets.*} lemma (in topgroup) local_iff_neutral: assumes "∀U∈T∩𝒩⇩_{0}. ∃N∈𝒩⇩_{0}. N⊆U∧ P(N,T)" "∀N∈Pow(G). ∀x∈G. P(N,T) ⟶ P(x\<ltr>N,T)" shows "T{is locally}P" proof- { fix x U assume "x∈⋃T""U∈T""x∈U" then have "(\<rm>x)\<ltr>U∈T∩𝒩⇩_{0}" using open_tr_open(1) open_trans_neigh neg_in_tgroup unfolding G_def by auto with assms(1) obtain N where "N⊆((\<rm>x)\<ltr>U)""P(N,T)""N∈𝒩⇩_{0}" by auto note `x∈⋃T``N⊆((\<rm>x)\<ltr>U)` moreover from `U∈T` have "U⊆⋃T" by auto moreover from `N∈𝒩⇩_{0}` have "N⊆G" unfolding zerohoods_def by auto ultimately have "(x\<ltr>N)⊆U" using trans_subset unfolding G_def by auto moreover from `N⊆G``x∈⋃T` assms(2) `P(N,T)` have "P((x\<ltr>N),T)" unfolding G_def by auto moreover from `N∈𝒩⇩_{0}``x∈⋃T` have "x∈int(x\<ltr>N)" using elem_in_int_trans unfolding G_def by auto ultimately have "∃N∈Pow(U). x∈int(N)∧P(N,T)" by auto } then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] by auto qed lemma (in topgroup) trans_closed: assumes "A{is closed in}T""x∈G" shows "(x\<ltr>A){is closed in}T" proof- from assms(1) have "cl(A)=A" using Top_3_L8 unfolding IsClosed_def by auto then have "x\<ltr>cl(A)=x\<ltr>A" by auto then have "cl(x\<ltr>A)=x\<ltr>A" using trans_closure assms unfolding IsClosed_def by auto moreover have "x\<ltr>A⊆G" unfolding ltrans_def using group0.group0_5_L1(2)[OF group0_valid_in_tgroup `x∈G`] unfolding image_def range_def domain_def converse_def Pi_def by auto ultimately show ?thesis using Top_3_L8 unfolding G_def by auto qed text{*As it is written in the previous section, every topological group is regular.*} theorem (in topgroup) topgroup_reg: shows "T{is regular}" proof- { fix U assume "U∈T∩𝒩⇩_{0}" then obtain V where "cl(V)⊆U""V∈𝒩⇩_{0}" using exist_basehoods_closed by blast then have "V⊆cl(V)" using cl_contains_set unfolding zerohoods_def G_def by auto then have "int(V)⊆int(cl(V))" using interior_mono by auto with `V∈𝒩⇩_{0}` have "cl(V)∈𝒩⇩_{0}" unfolding zerohoods_def G_def using Top_3_L11(1) by auto from `V∈𝒩⇩_{0}` have "cl(V){is closed in}T" using cl_is_closed unfolding zerohoods_def G_def by auto with `cl(V)∈𝒩⇩_{0}``cl(V)⊆U` have "∃N∈𝒩⇩_{0}. N⊆U∧N{is closed in}T" by auto } then have "∀U∈T∩𝒩⇩_{0}. ∃N∈𝒩⇩_{0}. N⊆U∧N{is closed in}T" by auto moreover have "∀N∈Pow(G).( ∀x∈G. (N{is closed in}T⟶(x\<ltr>N){is closed in}T))" using trans_closed by auto ultimately have "T{is locally-closed}" using local_iff_neutral unfolding IsLocallyClosed_def by auto then show "T{is regular}" using regular_locally_closed by auto qed text{*The promised corollary follows:*} corollary (in topgroup) T2_imp_T3: assumes "T{is T⇩_{2}}" shows "T{is T⇩_{3}}" using T2_is_T1 topgroup_reg isT3_def assms by auto end