Theory Topological_Group

✐‹creator "Niklas Krofta"›
section ‹General theory of Topological Groups›
theory Topological_Group
  imports 
    "HOL-Algebra.Group" 
    "HOL-Algebra.Coset"
    "HOL-Analysis.Abstract_Topology" 
    "HOL-Analysis.Product_Topology" 
    "HOL-Analysis.T1_Spaces"
    "HOL-Analysis.Abstract_Metric_Spaces"
     Uniform_Structure 
begin

paragraph ‹Summary›
text ‹
  In this section we define topological groups and prove basic results about them.
  We also introduce the left and right uniform structures of topological groups and
  prove the Birkhoff-Kakutani theorem.
›

subsection ‹Auxiliary definitions and results›
subsubsection ‹Miscellaneous›

lemma connected_components_homeo:
  assumes homeo: "homeomorphic_map T1 T2 φ" and in_space: "x  topspace T1"
  shows "φ`(connected_component_of_set T1 x) = connected_component_of_set T2 (φ x)"
proof
  let ?Z = connected_component_of_set
  show "φ`(?Z T1 x)  ?Z T2 (φ x)"
    by (metis connected_component_of_eq connected_component_of_maximal connectedin_connected_component_of homeo homeomorphic_map_connectedness_eq imageI in_space mem_Collect_eq)
next
  let ?Z = connected_component_of_set
  from homeo obtain ψ where ψ_homeo: "homeomorphic_map T2 T1 ψ"
    and ψ_inv: "(y  topspace T1. ψ (φ y) = y)  (y  topspace T2. φ (ψ y) = y)"
    by (smt (verit) homeomorphic_map_maps homeomorphic_maps_map)
  from homeo in_space have "φ x  topspace T2"
    using homeomorphic_imp_surjective_map by blast
  then have "ψ`(?Z T2 (φ x))  ?Z T1 (ψ (φ x))"
    by (metis connected_component_of_eq connected_component_of_maximal connectedin_connected_component_of ψ_homeo homeomorphic_map_connectedness_eq imageI mem_Collect_eq)
  then show "?Z T2 (φ x)  φ`(?Z T1 x)"
    by (smt (verit, del_insts) ψ_inv connected_component_of_subset_topspace image_subset_iff in_space subsetD subsetI)
qed

lemma open_map_prod_top:
  assumes "open_map T1 T3 f" and "open_map T2 T4 g"
  shows "open_map (prod_topology T1 T2) (prod_topology T3 T4) (λ(x, y). (f x, g y))"
proof (unfold open_map_def, standard, standard)
  let ?p = "λ(x, y). (f x, g y)"
  fix U assume "openin (prod_topology T1 T2) U"
  then obtain 𝒰 where h𝒰: "𝒰  {V × W | V W. openin T1 V  openin T2 W}   𝒰 = U"
    unfolding openin_prod_topology union_of_def using arbitrary_def by auto
  then have "?p`U =  {?p`VW | VW. VW  𝒰}" by blast
  then have "?p`U =  {?p`(V × W) | V W. V × W  𝒰  openin T1 V  openin T2 W}" 
    using h𝒰 by blast
  moreover have "?p`(V × W) = (f`V) × (g`W)" for V W by fast
  ultimately have "?p`U =  {(f`V) × (g`W) | V W. V × W  𝒰  openin T1 V  openin T2 W}" by presburger
  moreover have "openin (prod_topology T3 T4) ((f`V) × (g`W))" if "openin T1 V  openin T2 W" for V W
    using openin_prod_Times_iff assms that open_map_def by metis
  ultimately show "openin (prod_topology T3 T4) (?p`U)" by fastforce
qed

lemma injective_quotient_map_homeo:
  assumes "quotient_map T1 T2 q" and inj: "inj_on q (topspace T1)"
  shows "homeomorphic_map T1 T2 q" using assms
    unfolding homeomorphic_eq_everything_map injective_quotient_map[OF inj] by fast

lemma (in group) subgroupI_alt:
  assumes subset: "H  carrier G" and nonempty: "H  {}" and 
    closed: "σ τ. σ  H  τ  H  σ  inv τ  H"
  shows "subgroup H G"
proof -
  from nonempty obtain η where "η  H" by blast
  then have "𝟭  H" using closed[of η η] subset r_inv by fastforce
  then have closed_inv: "inv σ  H" if "σ  H" for σ
    using closed[of 𝟭 σ] r_inv r_one subset that by force
  then have "σ  τ  H" if "σ  H  τ  H" for σ τ
    using closed[of σ "inv τ"] inv_inv subset subset_iff that by auto
  then show ?thesis using assms closed_inv by (auto intro: subgroupI)
qed

lemma subgroup_intersection: 
  assumes "subgroup H G" and "subgroup H' G"
  shows "subgroup (H  H') G"
  using assms unfolding subgroup_def by force

subsubsection ‹Quotient topology›

definition quot_topology :: "'a topology  ('a  'b)  'b topology" where
"quot_topology T q = topology (λU. U  q`(topspace T)  openin T {x  topspace T. q x  U})"

lemma quot_topology_open:
  fixes T :: "'a topology" and q :: "'a  'b"
  defines "openin_quot U  U  q`(topspace T)  openin T {x  topspace T. q x  U}"
  shows "openin (quot_topology T q) = openin_quot"
proof -
  have "istopology openin_quot"
  proof -
    have "openin_quot (U1  U2)" if "openin_quot U1  openin_quot U2" for U1 U2
    proof -
      have "{x  topspace T. q x  U1  U2} = {x  topspace T. q x  U1}  {x  topspace T. q x  U2}" by blast
      then show ?thesis using that unfolding openin_quot_def by auto
    qed
    moreover have "openin_quot ( 𝒰)" if "U𝒰. openin_quot U" for 𝒰
    proof -
      have "{x  topspace T. q x   𝒰} =  {{x  topspace T. q x  U} | U. U  𝒰}" by blast
      then show ?thesis using that unfolding openin_quot_def by auto
    qed
    ultimately show ?thesis using istopology_def
      by (smt (verit) Collect_cong Sup_set_def UnionI Union_iff image_eqI mem_Collect_eq mem_Collect_eq openin_topspace subsetI subset_antisym topspace_def)
  qed
  from topology_inverse'[OF this] show ?thesis using quot_topology_def unfolding openin_quot_def by metis
qed

lemma projection_quotient_map: "quotient_map T (quot_topology T q) q" 
proof (unfold quotient_map_def, intro conjI)
  have "openin (quot_topology T q) (q ` topspace T)" using quot_topology_open
    by (smt (verit) image_subset_iff mem_Collect_eq openin_subtopology_refl subsetI subtopology_superset)
  then show "q ` topspace T = topspace (quot_topology T q)" using quot_topology_open
    by (metis (no_types, opaque_lifting) openin_subset openin_topspace subset_antisym)
next
  show "U  topspace (quot_topology T q).
       openin T {x  topspace T. q x  U} = openin (quot_topology T q) U"
    using quot_topology_open by (metis (mono_tags, lifting) openin_topspace order_trans)
qed

corollary topspace_quot_topology [simp]: "topspace (quot_topology T q) = q`(topspace T)"
  using projection_quotient_map quotient_imp_surjective_map by metis

corollary projection_continuous: "continuous_map T (quot_topology T q) q"
  using projection_quotient_map quotient_imp_continuous_map by fast

subsection ‹Definition and basic results›

locale topological_group = group +
  fixes T :: "'g topology"
  assumes group_is_space [simp]: "topspace T = carrier G"
  assumes inv_continuous: "continuous_map T T (λσ. inv σ)"
  assumes mul_continuous: "continuous_map (prod_topology T T) T (λ(σ,τ). στ)"
begin

lemma in_space_iff_in_group [iff]: "σ  topspace T  σ  carrier G" 
  by auto

lemma translations_continuous [intro]:
  assumes in_group: "σ  carrier G"
  shows "continuous_map T T (λτ. στ)" and "continuous_map T T (λτ. τσ)"
proof -
  have "continuous_map T (prod_topology T T) (λτ. (σ,τ))"
    by (auto intro: continuous_map_pairedI simp: in_group)
  moreover have "(λτ. στ) = (λ(σ,τ). στ)  (λτ. (σ,τ))" by auto
  ultimately show "continuous_map T T (λτ. στ)"
    using mul_continuous continuous_map_compose by metis
next
  have "continuous_map T (prod_topology T T) (λτ. (τ,σ))"
    by (auto intro: continuous_map_pairedI simp: in_group)
  moreover have "(λτ. τσ) = (λ(σ,τ). στ)  (λτ. (τ,σ))" by auto
  ultimately show "continuous_map T T (λτ. τσ)"
    using mul_continuous continuous_map_compose by metis
qed

lemma translations_homeos:
  assumes in_group: "σ  carrier G"
  shows "homeomorphic_map T T (λτ. στ)" and "homeomorphic_map T T (λτ. τσ)"
proof -
  have "τtopspace T. inv σ  (σ  τ) = τ" by (simp add: group.inv_solve_left' in_group)
  moreover have "τtopspace T. σ  (inv σ  τ) = τ"
    by (metis group_is_space in_group inv_closed l_one m_assoc r_inv)
  ultimately have "homeomorphic_maps T T (λτ. στ) (λτ. (inv σ)τ)"
    using homeomorphic_maps_def in_group by blast
  then show "homeomorphic_map T T (λτ. στ)" using homeomorphic_maps_map by blast
next
  have "τtopspace T. τ  σ  inv σ = τ"
    by (simp add: group.inv_solve_right' in_group)
  moreover have "τtopspace T. τ  inv σ  σ = τ" by (simp add: in_group m_assoc)
  ultimately have "homeomorphic_maps T T (λτ. τσ) (λτ. τ(inv σ))"
    using homeomorphic_maps_def in_group by blast
  then show "homeomorphic_map T T (λτ. τσ)" using homeomorphic_maps_map by blast
qed

abbreviation conjugation :: "'g  'g  'g" where
"conjugation σ τ  σ  τ  inv σ"

corollary conjugation_homeo:
  assumes in_group: "σ  carrier G"
  shows "homeomorphic_map T T (conjugation σ)"
proof -
  have "conjugation σ = (λτ. τ  inv σ)  (λτ. σ  τ)" by auto
  then show ?thesis using translations_homeos homeomorphic_map_compose
    by (metis in_group inv_closed)
qed

corollary open_set_translations:
  assumes open_set: "openin T U" and in_group: "σ  carrier G"
  shows "openin T (σ <# U)" and "openin T (U #> σ)"
proof -
  let  = "λτ. σ  τ"
  have "σ <# U = `U" unfolding l_coset_def by blast
  then show "openin T (σ <# U)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_openness_eq open_set)
next
  let  = "λτ. τ  σ"
  have "U #> σ = `U" unfolding r_coset_def by fast
  then show "openin T (U #> σ)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_openness_eq open_set)
qed

corollary closed_set_translations:
  assumes closed_set: "closedin T U" and in_group: "σ  carrier G"
  shows "closedin T (σ <# U)" and "closedin T (U #> σ)"
proof -
  let  = "λτ. στ"
  have "σ <# U = `U" unfolding l_coset_def by fast
  then show "closedin T (σ <# U)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_closedness_eq closed_set)
next
  let  = "λτ. τσ"
  have "U #> σ = `U" unfolding r_coset_def by fast
  then show "closedin T (U #> σ)" using translations_homeos[OF in_group]
    by (metis homeomorphic_map_closedness_eq closed_set)
qed

lemma inverse_homeo: "homeomorphic_map T T (λσ. inv σ)"
  using homeomorphic_map_involution[OF inv_continuous] by auto

subsection ‹Subspaces and quotient spaces›

abbreviation connected_component_1 :: "'g set" where
"connected_component_1  connected_component_of_set T 𝟭"

lemma connected_component_1_props: 
  shows "connected_component_1  G" and "closedin T connected_component_1"
proof -
  let ?Z = "connected_component_of_set T"
  have in_space: "(?Z 𝟭)  topspace T"
    using connected_component_of_subset_topspace by fastforce
  have "subgroup (?Z 𝟭) G"
  proof (rule subgroupI)
    show "(?Z 𝟭)  carrier G" using in_space by auto
  next
    show "(?Z 𝟭)  {}"
      by (metis connected_component_of_eq_empty group_is_space one_closed)
  next
    fix σ assume : "σ  (?Z 𝟭)"
    let  = "λη. inv η"
    have "`(?Z 𝟭) = ?Z 𝟭" using connected_components_homeo
      by (metis group_is_space inv_one inverse_homeo one_closed)
    then show "inv σ  (?Z 𝟭)" using  by blast
  next
    fix σ τ assume : "σ  (?Z 𝟭)" and : "τ  (?Z 𝟭)"
    let  = "λη. σ  η"
    have "`(?Z 𝟭) = ?Z σ" using connected_components_homeo
      by (metis group_is_space  in_space one_closed r_one subset_eq translations_homeos(1))
    moreover have "?Z σ = ?Z 𝟭" using  by (simp add: connected_component_of_equiv)
    ultimately show "σ  τ  ?Z 𝟭" using  by blast
  qed
  moreover have "conjugation σ τ  ?Z 𝟭" if hστ: "σ  carrier G  τ  ?Z 𝟭" for σ τ
  proof -
    let  = "conjugation σ"
    have "`(?Z 𝟭) = ?Z ( 𝟭)" using connected_components_homeo
      by (metis conjugation_homeo group_is_space one_closed hστ)
    then show ?thesis using r_inv r_one hστ by auto
  qed
  ultimately show "connected_component_1  G" using normal_inv_iff by blast
next
  show "closedin T connected_component_1" by (simp add: closedin_connected_component_of)
qed

lemma group_prod_space [simp]: "topspace (prod_topology T T) = (carrier G) × (carrier G)"
  by auto

no_notation eq_closure_of (closure'_ofı›)

lemma subgroup_closure:
  assumes H_subgroup: "subgroup H G"
  shows "subgroup (T closure_of H) G"
proof -
  have subset: "T closure_of H  carrier G"
    by (metis closedin_closure_of closedin_subset group_is_space)
  have nonempty: "T closure_of H  {}"
    by (simp add: assms closure_of_eq_empty group.subgroupE(1) subgroupE(2))
  
  let  = "λ(σ,τ). σ  inv τ"
  have φ_continuous: "continuous_map (prod_topology T T) T "
  proof -
    have "continuous_map (prod_topology T T) (prod_topology T T) (λ(σ, τ). (σ, inv τ))"
      using continuous_map_prod_top inv_continuous by fastforce
    moreover have " = (λ(σ, τ). σ  τ)  (λ(σ, τ). (σ, inv τ))" by fastforce
    ultimately show ?thesis using mul_continuous continuous_map_compose by force
  qed

  have "σ  inv τ  T closure_of H" 
    if hστ: "σ  T closure_of H  τ  T closure_of H" for σ τ
  proof -
    have in_space: "σ  inv τ  topspace T" using subset hστ by fast
    have "η  H. η  U" if hU: "openin T U  σ  inv τ  U" for U
    proof -
      let ?V = "{x  topspace (prod_topology T T).  x  U}"
      have "openin (prod_topology T T) ?V" 
        using φ_continuous hU openin_continuous_map_preimage by blast
      moreover have "(σ,τ)  ?V"
        using hU group_prod_space hστ subset by force
      ultimately obtain V1 V2 where 
        hV1V2: "openin T V1  openin T V2  σ  V1  τ  V2  V1 × V2  ?V"
        by (smt (verit) openin_prod_topology_alt) 
      then obtain σ' τ' where hσ'τ': "σ'  V1  H  τ'  V2  H" using hστ
        by (meson all_not_in_conv disjoint_iff openin_Int_closure_of_eq_empty)
      then have " (σ',τ')  U" using hV1V2 by blast
      moreover have " (σ',τ')  H" using hσ'τ' H_subgroup subgroupE(3,4) by simp
      ultimately show ?thesis by blast
    qed
    then show ?thesis using closure_of_def in_space by force
  qed
  then show ?thesis using subgroupI_alt subset nonempty by blast
qed

lemma normal_subgroup_closure:
  assumes normal_subgroup: "N  G"
  shows "(T closure_of N)  G"
proof -
  have "(conjugation σ)`(T closure_of N)  T closure_of N" if : "σ  carrier G" for σ 
  proof -
    have "(conjugation σ)`N  N" using normal_subgroup normal_invE(2)  by auto
    then have "T closure_of (conjugation σ)`N  T closure_of N" 
      using closure_of_mono by meson
    moreover have "(conjugation σ)`(T closure_of N)  T closure_of (conjugation σ)`N"
      using  conjugation_homeo
      by (meson continuous_map_eq_image_closure_subset homeomorphic_imp_continuous_map)
    ultimately show ?thesis by blast
  qed
  moreover have "subgroup (T closure_of N) G" using subgroup_closure
    by (simp add: normal_invE(1) normal_subgroup)
  ultimately show ?thesis using normal_inv_iff by auto
qed

lemma topological_subgroup:
  assumes "subgroup H G"
  shows "topological_group (G carrier := H) (subtopology T H)"
proof -
  interpret subgroup H G by fact
  let ?ℋ = "(G carrier := H)" and ?T' = "subtopology T H"
  have H_subspace: "topspace ?T' = H" using topspace_subtopology_subset by force
  have "continuous_map ?T' T (λσ. inv σ)" using continuous_map_from_subtopology inv_continuous by blast
  moreover have "(λσ. inv σ)  topspace ?T'  H" unfolding Pi_def H_subspace by blast
  ultimately have "continuous_map ?T' ?T' (λσ. inv σ)" using continuous_map_into_subtopology by blast
  then have sub_inv_continuous: "continuous_map ?T' ?T' (λσ. inv?ℋσ)"
    using continuous_map_eq H_subspace m_inv_consistent assms by fastforce
  have "continuous_map (prod_topology ?T' ?T') T (λ(σ,τ). σ  τ)" 
    unfolding subtopology_Times[symmetric] using continuous_map_from_subtopology[OF mul_continuous] by fast
  moreover have "(λ(σ,τ). σ  τ)  topspace (prod_topology ?T' ?T')  H" 
    unfolding Pi_def topspace_prod_topology H_subspace by fast
  ultimately have "continuous_map (prod_topology ?T' ?T') ?T' (λ(σ,τ). σ  τ)"
    using continuous_map_into_subtopology by blast
  then have "continuous_map (prod_topology ?T' ?T') ?T' (λ(σ,τ). σ ?ℋτ)" by fastforce
  then show ?thesis unfolding topological_group_def topological_group_axioms_def using H_subspace sub_inv_continuous by auto
qed

text ‹Topology on the set of cosets of some subgroup›

abbreviation coset_topology :: "'g set  'g set topology" where
"coset_topology H  quot_topology T (r_coset G H)"

lemma coset_topology_topspace[simp]:
  shows "topspace (coset_topology H) = (r_coset G H)`(carrier G)"
  using projection_quotient_map quotient_imp_surjective_map group_is_space by metis

lemma projection_open_map:
  assumes subgroup: "subgroup H G"
  shows "open_map T (coset_topology H) (r_coset G H)"
proof (unfold open_map_def, standard, standard)
  fix U assume hU: "openin T U"
  let  = "r_coset G H"
  let ?V = "{σ  topspace T.  σ  `U}"
  have subsets: "H  carrier G  U  carrier G"
    using subgroup hU  openin_subset by (force elim!: subgroupE)
  have "?V = {σ  carrier G. τ  U. H #> σ = H #> τ}" using image_def by blast 
  then have "?V = {σ  carrier G. τ  U. σ  H #> τ}" using subsets 
    by (smt (verit) Collect_cong rcos_self repr_independence subgroup subset_eq)
  also have "... = (η  H. η <# U)" unfolding r_coset_def l_coset_def using subsets by auto
  moreover have "openin T (η <# U)" if "η  H" for η
    using open_set_translations(1)[OF hU] subsets that by blast
  ultimately have "openin T ?V" by fastforce
  then show "openin (coset_topology H) (`U)" using quot_topology_open hU
    by (metis (mono_tags, lifting) Collect_cong image_mono openin_subset)
qed

lemma topological_quotient_group:
  assumes normal_subgroup: "N  G"
  shows "topological_group (G Mod N) (coset_topology N)"
proof -
  interpret normal N G by fact
  let  = "r_coset G N"
  let ?T' = "coset_topology N"
  have quot_space: "topspace ?T' = `(carrier G)" using coset_topology_topspace by presburger
  then have quot_group_quot_space: "topspace ?T' = carrier (G Mod N)" using carrier_FactGroup by metis

  let ?quot_mul = "λ(, ).  G Mod N"
  have π_prod_space: "topspace (prod_topology ?T' ?T') = `(carrier G) × `(carrier G)"
    using quot_space topspace_prod_topology by simp
  have quot_mul_continuous: "continuous_map (prod_topology ?T' ?T') ?T' ?quot_mul"
  proof (unfold continuous_map_def, intro conjI ballI allI impI)
    show "?quot_mul  topspace (prod_topology ?T' ?T')  topspace ?T'" 
      using rcos_sum unfolding quot_space π_prod_space by auto
  next
    fix U assume hU: "openin ?T' U"
    let ?V = "{p  topspace (prod_topology ?T' ?T'). ?quot_mul p  U}"
    let ?W = "{(σ,τ)  topspace (prod_topology T T). N #> (σ  τ)  U}"
    let 2 = "λ(σ, τ). (N #> σ, N #> τ)"
    have "(λ(σ,τ). N #> (σ  τ)) =   (λ(σ,τ). σ  τ)" by fastforce
    then have "continuous_map (prod_topology T T) ?T' (λ(σ,τ). N #> (σ  τ))"
      using continuous_map_compose mul_continuous projection_continuous by fastforce
    then have "openin (prod_topology T T) ?W"
      using hU openin_continuous_map_preimage
      by (smt (verit) Collect_cong case_prodE case_prodI2 case_prod_conv)
    moreover have "open_map (prod_topology T T) (prod_topology ?T' ?T') 2"
      using projection_open_map open_map_prod_top by (metis subgroup_axioms)
    ultimately have "openin (prod_topology ?T' ?T') (2`?W)" using open_map_def by blast
    moreover have "?V = 2`?W"
      using rcos_sum unfolding π_prod_space group_prod_space by auto
    ultimately show "openin (prod_topology ?T' ?T') ?V" by presburger
  qed

  let ?quot_inv = "λ. invG Mod N"
  have π_inv: "?quot_inv (N #> σ) =  (inv σ)" if "σ  carrier G" for σ 
    using inv_FactGroup rcos_inv carrier_FactGroup that by blast 
  have "continuous_map ?T' ?T' ?quot_inv"
  proof (unfold continuous_map_def, intro conjI ballI allI impI)
    show "?quot_inv  topspace ?T'  topspace ?T'" using π_inv quot_space by auto
  next
    fix U assume hU: "openin ?T' U"
    let ?V = "{  topspace ?T'. ?quot_inv   U}"
    let ?W = "{σ  topspace T. N #> (inv σ)  U}"
    have "(λσ. N #> (inv σ)) =   (λσ. inv σ)" by fastforce
    then have "continuous_map T ?T' (λσ. N #> (inv σ))"
      using continuous_map_compose projection_continuous inv_continuous 
      by (metis (no_types, lifting)) 
    then have "openin T ?W" using hU openin_continuous_map_preimage by blast
    then have "openin ?T' (`?W)" 
      using projection_open_map by (simp add: open_map_def subgroup_axioms)
    moreover have "?V = `?W" using π_inv quot_space by force
    ultimately show "openin ?T' ?V" by presburger
  qed

  then show ?thesis unfolding topological_group_def topological_group_axioms_def
    using quot_group_quot_space quot_mul_continuous factorgroup_is_group by blast
qed

text ‹
  See cite"stackexchange_quot_groups" for our approach to proving that quotient groups
  of topological groups are topological.
›

abbreviation neighborhood :: "'g  'g set  bool" where
"neighborhood σ U  openin T U  σ  U"

abbreviation symmetric :: "'g set  bool" where
"symmetric S  {inv σ | σ. σ  S}  S"

text 
  ‹Note that this implies the other inclusion, so symmetric subsets are equal to their 
  image under inversion.
›

lemma neighborhoods_of_1:
  assumes "neighborhood 𝟭 U"
  shows "V. neighborhood 𝟭 V  symmetric V  V <#> V  U"
proof -
  have a: "VU'. neighborhood 𝟭 V  symmetric V" if hU': "neighborhood 𝟭 U'" for U'
  proof -
    let ?W = "{σ  carrier G. inv σ  U'}"
    let ?V = "?W  ((λσ. inv σ)`?W)"
    have "neighborhood 𝟭 ?W" using openin_continuous_map_preimage[OF inv_continuous]
        hU' inv_one by fastforce
    moreover from this have "neighborhood 𝟭 ((λσ. inv σ)`?W)" using inverse_homeo 
        homeomorphic_imp_open_map inv_one image_eqI open_map_def by (metis (mono_tags, lifting))
    ultimately have neighborhood: "neighborhood 𝟭 ?V" by blast
    have "inv σ  ?V" if "σ  ?V" for σ using that by auto
    then have "symmetric ?V" by fast
    moreover have "σ  U'" if "σ  ?V" for σ using that by blast
    ultimately show ?thesis using neighborhood by blast
  qed
  have b: "V. neighborhood 𝟭 V  V <#> V  U'" if hU': "neighborhood 𝟭 U'" for U' 
  proof -
    let ?W = "{(σ,τ)  carrier G × carrier G. στ  U'}"
    have preimage_mul: "?W = {x  topspace (prod_topology T T). (λ(σ,τ). στ) x  U'}"
      using topspace_prod_topology by fastforce
    then have "openin (prod_topology T T) ?W  (𝟭,𝟭)  ?W" 
      using openin_continuous_map_preimage[OF mul_continuous] hU' r_one by fastforce
    then obtain W1 W2 where hW1W2: "neighborhood 𝟭 W1  neighborhood 𝟭 W2  W1×W2?W"
      using openin_prod_topology_alt[where S="?W"] by meson
    let ?V = "W1  W2"
    from hW1W2 have "neighborhood 𝟭 ?V" by fast
    moreover have "στ  U'" if "σ?V  τ?V" for σ τ using preimage_mul hW1W2 that by blast
    ultimately show ?thesis unfolding set_mult_def by blast
  qed
  from b[OF assms] obtain W where hW: "neighborhood 𝟭 W  W <#> W  U" by presburger
  from this a obtain V where "VW  neighborhood 𝟭 V  symmetric V" by presburger
  moreover from this have "V <#> V  U" using hW mono_set_mult by blast
  ultimately show ?thesis unfolding set_mult_def by blast
qed

lemma Hausdorff_coset_space:
  assumes subgroup: "subgroup H G" and H_closed: "closedin T H"
  shows "Hausdorff_space (coset_topology H)"
proof (unfold Hausdorff_space_def, intro allI impI)
  interpret subgroup H G by fact
  let  = "r_coset G H"
  let ?T' = "coset_topology H"
  fix   assume cosets: "  topspace ?T'    topspace ?T'    "
  then obtain σ τ where hστ: "σ  carrier G  τ  carrier G   = H #> σ   = H #> τ" by auto
  then have "σ  H #> τ" using cosets subgroup repr_independence by blast
  have "𝟭  (inv σ) <# (H #> τ)" 
  proof
    assume "𝟭  inv σ <# (H #> τ)"
    then obtain η where : "η  H  𝟭 = (inv σ)  (η  τ)" unfolding r_coset_def l_coset_def by auto
    then have "σ = η  τ"
      by (metis (no_types, lifting) Units_eq Units_m_closed group.inv_comm group_l_invI hστ inv_closed inv_inv inv_unique' l_inv_ex mem_carrier)
    then show "False" using σ  H #> τ  r_coset_def by fast
  qed
  let ?U = "topspace T - ((inv σ) <# (H #> τ))"
  have "closedin T ((inv σ) <# (H #> τ))" 
      using closed_set_translations closed_set_translations[OF H_closed] hστ by simp
  then have "neighborhood 𝟭 ?U" using 𝟭  (inv σ) <# (H #> τ) by blast
  then obtain V where hV: "neighborhood 𝟭 V  symmetric V  V <#> V  ?U"
    using neighborhoods_of_1 by presburger
  let ?V1 = "σ <# V" and ?V2 = "τ <# V"
  have disjoint: "`?V1  `?V2 = {}"
  proof (rule ccontr)
    assume "`?V1  `?V2  {}"
    then obtain υ1 υ2 where 1υ2: "υ1  V  υ2  V   (συ1) =  (τυ2)" 
      unfolding l_coset_def by auto
    moreover then have υ1υ2_in_group: "υ1  carrier G  υ2  carrier G" 
      using hV openin_subset by force
    ultimately have in_H: "(συ1)  inv (τυ2)  H" 
      using subgroup repr_independenceD rcos_module_imp hστ m_closed 
      by (metis group.rcos_self is_group subgroup.m_closed subgroup_self)
    let  = "(συ1)  inv (τυ2)"
    have " = σ  (υ1  inv υ2)  inv τ" using hστ υ1υ2_in_group m_assoc
      by (simp add: inv_mult_group subgroupE(4) subgroup_self)
    then have "inv σ  (  τ) = υ1  inv υ2" 
      using hστ υ1υ2_in_group m_assoc inv_solve_left' by auto
    then have "υ1  inv υ2  (inv σ) <# (H #> τ)" 
      unfolding l_coset_def r_coset_def using hστ inv_closed in_H by force
    moreover have "υ1  inv υ2  ?U" using 1υ2 hV unfolding set_mult_def by blast
    ultimately show "False" by force 
  qed
  have "neighborhood σ ?V1  neighborhood τ ?V2"
    using open_set_translations[of V] l_coset_def hV hστ r_one by force
  then have "openin ?T' (`?V1)  openin ?T' (`?V2)    `?V1    `?V2"
    using projection_open_map open_map_def subgroup hστ by fast
  then show "W1 W2. openin ?T' W1  openin ?T' W2    W1    W2  disjnt W1 W2"
    using disjoint disjnt_def by meson
qed

lemma Hausdorff_coset_space_converse:
  assumes subgroup: "subgroup H G"
  assumes Hausdorff: "Hausdorff_space (coset_topology H)"
  shows "closedin T H"
proof -
  interpret subgroup H G by fact
  let ?T' = "coset_topology H"
  have "H  topspace ?T'" using coset_topology_topspace coset_join2[of 𝟭 H] subgroup by auto
  then have "closedin ?T' {H}" 
    using t1_space_closedin_singleton Hausdorff_imp_t1_space[OF Hausdorff] by fast
  then have preimage_closed: "closedin T {σ  carrier G. H #> σ = H}" 
    using projection_continuous closedin_continuous_map_preimage by fastforce
  have "σ  H  H #> σ = H" if "σ  carrier G" for σ
    using coset_join1 coset_join2 subgroup that by metis
  then have "H = {σ  carrier G. H #> σ = H}" using subset by auto
  then show ?thesis using preimage_closed by presburger
qed

corollary Hausdorff_coset_space_iff:
  assumes subgroup: "subgroup H G"
  shows "Hausdorff_space (coset_topology H)  closedin T H"
  using Hausdorff_coset_space Hausdorff_coset_space_converse subgroup by blast

corollary topological_group_hausdorff_iff_one_closed:
  shows "Hausdorff_space T  closedin T {𝟭}"
proof -
  let  = "r_coset G {𝟭}"
  have "inj_on  (carrier G)" unfolding inj_on_def r_coset_def by simp
  then have "homeomorphic_map T (coset_topology {𝟭}) "
    using projection_quotient_map injective_quotient_map_homeo group_is_space by metis
  then have "Hausdorff_space T  Hausdorff_space (coset_topology {𝟭})" 
    using homeomorphic_Hausdorff_space homeomorphic_map_imp_homeomorphic_space by blast
  then show ?thesis using Hausdorff_coset_space_iff triv_subgroup by blast
qed

lemma set_mult_one_subset:
  assumes "A  carrier G  B  carrier G" and "𝟭  B"
  shows "A  A <#> B" 
  unfolding set_mult_def using assms r_one by force

lemma open_set_mult_open:
  assumes "openin T U  S  carrier G"
  shows "openin T (S <#> U)"
proof -
  have "S <#> U = (σS. σ <# U)" unfolding set_mult_def l_coset_def by blast
  moreover have "openin T (σ <# U)" if "σ  S" for σ using open_set_translations(1) assms that by auto
  ultimately show ?thesis by auto
qed

lemma open_set_inv_open:
  assumes "openin T U"
  shows "openin T (set_inv U)"
proof -
  have "set_inv U = (λσ. inv σ)`U" unfolding image_def SET_INV_def by blast
  then show ?thesis using inverse_homeo homeomorphic_imp_open_map open_map_def assms by metis
qed

lemma open_set_in_carrier[elim]:
  assumes "openin T U"
  shows "U  carrier G"
  using openin_subset assms by force

subsection ‹Uniform structures›

abbreviation left_entourage :: "'g set  ('g × 'g) set" where
"left_entourage U  {(σ,τ)  carrier G × carrier G. inv σ  τ  U}"

abbreviation right_entourage :: "'g set  ('g × 'g) set" where
"right_entourage U  {(σ,τ)  carrier G × carrier G. σ  inv τ  U}"

definition left_uniformity :: "'g uniformity" where "left_uniformity =
  uniformity (carrier G, λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  left_entourage U  E))"

definition right_uniformity :: "'g uniformity" where "right_uniformity =
  uniformity (carrier G, λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  right_entourage U  E))"

lemma
  uspace_left_uniformity[simp]: "uspace left_uniformity = carrier G" (is ?space_def) and
  entourage_left_uniformity: "entourage_in left_uniformity = 
    (λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  left_entourage U  E))" (is ?entourage_def)
proof -
  let  = "λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  left_entourage U  E)"
  have " (carrier G × carrier G)" 
    using exI[where x="carrier G"] openin_topspace by force
  moreover have "Id_on (carrier G)  E   (E¯)  (F.  F  F O F  E)  
    (F. E  F  F  carrier G × carrier G   F)" if hE: " E" for E
  proof -
    from hE obtain U where hU: "neighborhood 𝟭 U  left_entourage U  E" by presburger
    then have U_subset: "U  carrier G" using openin_subset by force
    from hU have "Id_on (carrier G)  E" by fastforce
    moreover have " (E¯)"
    proof -
      have "(τ,σ)  E" if "σ  carrier G  τ  carrier G  inv σ  τ  set_inv U" for σ τ
      proof -
        have "inv τ  σ = inv (inv σ  τ)" using that inv_mult_group by auto
        from this have "inv τ  σ  U" using that inv_inv U_subset unfolding SET_INV_def by auto
        then show ?thesis using that hU by fast
      qed
      then have "left_entourage (set_inv U)  E¯" by blast 
      moreover have "neighborhood 𝟭 (set_inv U)" using inv_one hU open_set_inv_open SET_INV_def by fastforce
      ultimately show ?thesis using hE by auto
    qed
    moreover have "F.  F  F O F  E"
    proof -
      obtain V where hV: "neighborhood 𝟭 V  V <#> V  U"
        using neighborhoods_of_1 hU by meson
      let ?F = "left_entourage V"
      have "(σ,ρ)  E" if "(σ,τ)  ?F  (τ,ρ)  ?F" for σ τ ρ
      proof -
        have "σ  carrier G  τ  carrier G  ρ  carrier G" using that by force
        then have "inv σ  ρ = (inv σ  τ)  (inv τ  ρ)"
          using m_assoc inv_closed m_closed r_inv r_one by metis  
        moreover have "(inv σ  τ)  (inv τ  ρ)  U" using that hV unfolding set_mult_def by fast
        ultimately show ?thesis using hU that by force
      qed
      moreover have " ?F" using hV by blast
      ultimately show ?thesis using hV by auto
    qed
    moreover have "F. E  F  F  carrier G × carrier G   F" using hE by auto
    ultimately show ?thesis by blast
  qed
  moreover have " (E  F)" if hEF: " E   F" for E F
  proof -
    from hEF obtain U V where
      hU: "neighborhood 𝟭 U  left_entourage U  E" and
      hV: "neighborhood 𝟭 V  left_entourage V  F" by presburger
    then have "neighborhood 𝟭 (U  V)  left_entourage (U  V)  E  F" by fast
    then show ?thesis using that by auto
  qed
  ultimately have "uniformity_on (carrier G) "
    unfolding uniformity_on_def by auto
  from uniformity_inverse'[OF this] show ?space_def and ?entourage_def unfolding left_uniformity_def by auto
qed

lemma
  uspace_right_uniformity[simp]: "uspace right_uniformity = carrier G" (is ?space_def) and
  entourage_right_uniformity: "entourage_in right_uniformity =  
    (λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  right_entourage U  E))" (is ?entourage_def)
proof -
  let  = "λE. E  carrier G × carrier G  (U. neighborhood 𝟭 U  right_entourage U  E)"
  have " (carrier G × carrier G)" 
    using exI[where x="carrier G"] openin_topspace by force
  moreover have "Id_on (carrier G)  E   (E¯)  (F.  F  F O F  E)  
    (F. E  F  F  carrier G × carrier G   F)" if hE: " E" for E
  proof -
    from hE obtain U where 
      hU: "neighborhood 𝟭 U  right_entourage U  E"
      by presburger
    then have U_subset: "U  carrier G" using openin_subset by force
    from hU have "Id_on (carrier G)  E" by fastforce
    moreover have " (E¯)"
    proof -
      have "(τ,σ)  E" if "σ  carrier G  τ  carrier G  σ  inv τ  set_inv U" for σ τ
      proof -
        have "τ  inv σ = inv (σ  inv τ)" using that inv_mult_group by auto
        from this have "τ  inv σ  U" using that inv_inv U_subset unfolding SET_INV_def by auto
        then show ?thesis using that hU by fast
      qed
      then have "right_entourage (set_inv U)  E¯" by blast 
      moreover have "neighborhood 𝟭 (set_inv U)" using inv_one hU open_set_inv_open SET_INV_def by fastforce
      ultimately show ?thesis using hE by auto
    qed
    moreover have "F.  F  F O F  E"
    proof -
      obtain V where hV: "neighborhood 𝟭 V  V <#> V  U"
        using neighborhoods_of_1 hU by meson
      let ?F = "right_entourage V"
      have "(σ,ρ)  E" if "(σ,τ)  ?F  (τ,ρ)  ?F" for σ τ ρ
      proof -
        have "σ  carrier G  τ  carrier G  ρ  carrier G" using that by force
        then have "σ  inv ρ = (σ  inv τ)  (τ  inv ρ)"
          using m_assoc inv_closed m_closed l_inv r_one by metis  
        moreover have "(σ  inv τ)  (τ  inv ρ)  U" using that hV unfolding set_mult_def by fast
        ultimately show ?thesis using hU that by force
      qed
      moreover have " ?F" using hV by blast
      ultimately show ?thesis using hV by auto
    qed
    moreover have "F. E  F  F  carrier G × carrier G   F" using hE by auto
    ultimately show ?thesis by blast
  qed
  moreover have " (E  F)" if hEF: " E   F" for E F
  proof -
    from hEF obtain U V where
      hU: "neighborhood 𝟭 U  right_entourage U  E" and
      hV: "neighborhood 𝟭 V  right_entourage V  F"
      by presburger
    then have "neighborhood 𝟭 (U  V)  right_entourage (U  V)  E  F" by fast
    then show ?thesis using that by auto
  qed
  ultimately have "uniformity_on (carrier G) "
    unfolding uniformity_on_def by auto
  from uniformity_inverse'[OF this] show ?space_def and ?entourage_def unfolding right_uniformity_def by auto
qed

lemma left_uniformity_induces_group_topology [simp]:
  shows "utopology left_uniformity = T"
proof -
  let  = left_uniformity
  let ?T' = "utopology "
  have "openin T U  openin ?T' U" for U
  proof
    assume U_open: "openin T U"
    have "E. entourage_in  E  E``{σ}  U" if : "σ  U" for σ
    proof -
      let ?E = "left_entourage (inv σ <# U)"
      have in_group: "σ  carrier G" using  U_open open_set_in_carrier by blast
      then have "openin T (inv σ <# U)"
        using inv_closed open_set_translations(1) U_open by presburger
      then have "neighborhood 𝟭 (inv σ <# U)"
        using  in_group r_inv unfolding l_coset_def SET_INV_def by force
      then have "entourage_in  ?E" unfolding entourage_left_uniformity by blast
      moreover have "τ  U" if "τ  ?E``{σ}" for τ
      proof -
        from that have "inv σ  τ  inv σ <# U" by force
        then obtain ρ where : "ρ  U  inv σ  τ = inv σ  ρ" unfolding l_coset_def by fast
        then have "ρ  carrier G  τ  carrier G" using that open_set_in_carrier U_open by fast
        then have "τ = ρ" using in_group  inv_closed by (metis Units_eq Units_l_cancel)
        then show ?thesis using  by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover have "U  uspace " using openin_subset U_open by force
    ultimately show "openin ?T' U" unfolding openin_utopology by force
  next
    assume U_open: "openin ?T' U"
    have "W. neighborhood σ W  W  U" if : "σ  U" for σ
    proof -
      have in_group: "σ  carrier G" using  U_open openin_subset topspace_utopology by force
      from U_open  obtain E where hE: "entourage_in  E  E``{σ}  U"
        unfolding openin_utopology by blast
      then obtain V where hV: "neighborhood 𝟭 V  left_entourage V  E"
        unfolding entourage_left_uniformity by fastforce
      let ?W = "{τ  carrier G. inv σ  τ  V}"
      from hV have W_subset: "?W  E``{σ}" using in_group by fast
      have "continuous_map T T (λτ. inv σ  τ)" using translations_continuous in_group inv_closed by blast
      then have "openin T ?W" using openin_continuous_map_preimage hV by fastforce
      then have "neighborhood σ ?W" using in_group r_inv hV by simp
      then show ?thesis using W_subset hE by fast
    qed
    then show "openin T U" using openin_subopen by force
  qed
  then show ?thesis using topology_eq by blast
qed

lemma right_uniformity_induces_group_topology [simp]:
  shows "utopology right_uniformity = T"
proof -
  let  = right_uniformity
  let ?T' = "utopology "
  have "openin T U  openin ?T' U" for U
  proof
    assume U_open: "openin T U"
    have "E. entourage_in  E  E``{σ}  U" if : "σ  U" for σ
    proof -
      let ?E = "right_entourage (σ <# set_inv U)"
      have in_group: "σ  carrier G" using  U_open open_set_in_carrier by blast
      then have "openin T (σ <# set_inv U)"
        using open_set_inv_open open_set_translations(1) U_open by presburger
      then have "neighborhood 𝟭 (σ <# set_inv U)"
        using  in_group r_inv unfolding l_coset_def SET_INV_def by force
      then have "entourage_in  ?E" unfolding entourage_right_uniformity by blast
      moreover have "τ  U" if "τ  ?E``{σ}" for τ
      proof -
        from that have "σ  inv τ  σ <# set_inv U" by force
        then obtain ρ where : "ρ  U  σ  inv τ = σ  inv ρ"
          unfolding l_coset_def SET_INV_def by fast
        then have "ρ  carrier G  τ  carrier G" using that open_set_in_carrier U_open by fast
        then have "τ = ρ" using in_group  inv_closed by (metis Units_eq Units_l_cancel inv_inv)
        then show ?thesis using  by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover have "U  uspace " using openin_subset U_open by force
    ultimately show "openin ?T' U" unfolding openin_utopology by force
  next
    assume U_open: "openin ?T' U"
    have "W. neighborhood σ W  W  U" if : "σ  U" for σ
    proof -
      have in_group: "σ  carrier G" using  U_open openin_subset topspace_utopology by force
      from U_open  obtain E where hE: "entourage_in  E  E``{σ}  U"
        unfolding openin_utopology by blast
      then obtain V where hV: "neighborhood 𝟭 V  right_entourage V  E"
        unfolding entourage_right_uniformity by fastforce
      let ?W = "{τ  carrier G. σ  inv τ  V}"
      from hV have W_subset: "?W  E``{σ}" using in_group by fast
      have "(λτ. σ  inv τ) = (λτ. σ  τ)  (λτ. inv τ)" by fastforce
      then have "continuous_map T T (λτ. σ  inv τ)" using continuous_map_compose inv_continuous
          translations_continuous[OF in_group] by metis
      then have "openin T ?W" using openin_continuous_map_preimage hV by fastforce
      then have "neighborhood σ ?W" using in_group r_inv hV by simp
      then show ?thesis using W_subset hE by fast
    qed
    then show "openin T U" using openin_subopen by force
  qed
  then show ?thesis using topology_eq by blast
qed

lemma translations_ucontinuous:
  assumes in_group: "σ  carrier G"
  shows "ucontinuous left_uniformity left_uniformity (λτ. σ  τ)" and
    "ucontinuous right_uniformity right_uniformity (λτ. τ  σ)"
proof -
  let  = left_uniformity
  have "entourage_in  {(τ1, τ2)  uspace  × uspace . (σ  τ1, σ  τ2)  E}"
    if hE: "entourage_in  E" for E
  proof -
    let ?F = "{(τ1, τ2)  uspace  × uspace . (σ  τ1, σ  τ2)  E}"
    from hE obtain U where hU: "neighborhood 𝟭 U  left_entourage U  E"
      unfolding entourage_left_uniformity by auto
    have "(τ1, τ2)  ?F" if "τ1  carrier G  τ2  carrier G  inv τ1  τ2  U" for τ1 τ2
    proof -
      have "inv (σ  τ1)  (σ  τ2) = inv τ1  τ2"
        using that in_group m_closed inv_closed inv_mult_group m_assoc r_inv r_one
        by (smt (verit, ccfv_threshold))
      then have "(σ  τ1, σ  τ2)  E" using that hU in_group m_closed by fastforce
      then show ?thesis using that by auto
    qed
    then have "left_entourage U  ?F" by force
    then show ?thesis unfolding entourage_left_uniformity using hU by auto
  qed
  moreover have "(λτ. σ  τ)  uspace   uspace "
    unfolding Pi_def using uspace_left_uniformity in_group m_closed by force
  ultimately show "ucontinuous   (λτ. σ  τ)"
    unfolding ucontinuous_def by fast
next
  let  = right_uniformity
  have "entourage_in  {(τ1, τ2)  uspace  × uspace . (τ1  σ, τ2  σ)  E}"
    if hE: "entourage_in  E" for E
  proof -
    let ?F = "{(τ1, τ2)  uspace  × uspace . (τ1  σ, τ2  σ)  E}"
    from hE obtain U where hU: "neighborhood 𝟭 U  right_entourage U  E"
      unfolding entourage_right_uniformity by auto
    have "(τ1, τ2)  ?F" if "τ1  carrier G  τ2  carrier G  τ1  inv τ2  U" for τ1 τ2
    proof -
      have "(τ1  σ)  inv (τ2  σ) = τ1  inv τ2"
        using that in_group m_closed inv_closed inv_mult_group m_assoc r_inv r_one
        by (smt (verit, ccfv_threshold))
      then have "(τ1  σ, τ2  σ)  E" using that hU in_group m_closed by fastforce
      then show ?thesis using that by simp
    qed
    then have "right_entourage U  ?F" by force
    then show ?thesis unfolding entourage_right_uniformity using hU by auto
  qed
  moreover have "(λτ. τ  σ)  uspace   uspace "
    unfolding Pi_def using entourage_right_uniformity in_group m_closed by force
  ultimately show "ucontinuous   (λτ. τ  σ)" 
    unfolding ucontinuous_def by fast
qed

subsection ‹The Birkhoff-Kakutani theorem›
subsubsection ‹Prenorms on groups›

definition group_prenorm :: "('g  real)  bool" where
"group_prenorm N 
  N 𝟭 = 0 
  (σ τ. σ  carrier G  τ  carrier G  N (σ  τ)  N σ + N τ) 
  (σ  carrier G. N (inv σ) = N σ)"

lemma group_prenorm_clauses[elim]:
  assumes "group_prenorm N"
  obtains 
    "N 𝟭 = 0" and 
    "σ τ. σ  carrier G  τ  carrier G  N (σ  τ)  N σ + N τ" and 
    "σ. σ  carrier G  N (inv σ) = N σ"
  using assms unfolding group_prenorm_def by auto

proposition group_prenorm_nonnegative:
  assumes prenorm: "group_prenorm N"
  shows "σ  carrier G. N σ  0"
proof
  fix σ assume "σ  carrier G"
  from r_inv this have "0  N σ + N σ" using assms inv_closed group_prenorm_clauses by metis
  then show "N σ  0" by fastforce
qed

proposition group_prenorm_reverse_triangle_ineq:
  assumes prenorm: "group_prenorm N" and in_group: "σ  carrier G  τ  carrier G"
  shows "¦N σ - N τ¦  N (σ  inv τ)"
proof -
  have "σ = σ  inv τ  τ" using in_group inv_closed r_one l_inv m_assoc by metis
  then have a: "N σ  N (σ  inv τ) + N τ" using in_group inv_closed m_closed prenorm group_prenorm_clauses by metis
  have "inv τ = inv σ  (σ  inv τ)" using in_group inv_closed l_one l_inv m_assoc by metis 
  then have b: "N τ  N σ + N (σ  inv τ)" using in_group inv_closed m_closed prenorm group_prenorm_clauses by metis
  from a b show ?thesis by linarith
qed

definition induced_group_prenorm :: "('g  real)  'g  real" where
"induced_group_prenorm f σ = (SUP τ  carrier G. ¦f (τ  σ) - f τ¦)"
  
lemma induced_group_prenorm_welldefined:
  fixes f :: "'g  real"
  assumes f_bounded: "c.τ  carrier G. ¦f τ¦  c" and in_group: "σ  carrier G"
  shows "bdd_above ((λτ. ¦f (τ  σ) - f τ¦)`(carrier G))"
proof -
  from f_bounded obtain c where hc: "τ  carrier G. ¦f τ¦  c" by blast
  have "¦f (τ  σ) - f τ¦  2*c" if "τ  carrier G" for τ
  proof -
    have "¦f (τ  σ) - f τ¦  ¦f (τ  σ)¦ + ¦f τ¦" using abs_triangle_ineq by simp
    then show ?thesis using in_group that m_closed f_bounded hc by (smt (verit, best))
  qed
  then show ?thesis unfolding bdd_above_def image_def by blast
qed

lemma bounded_function_induces_group_prenorm:
  fixes f :: "'g  real"
  assumes f_bounded: "c.σ  carrier G. ¦f σ¦  c"
  shows "group_prenorm (induced_group_prenorm f)"
proof -
  let ?N = "λσ. SUP τ  carrier G. ¦f (τ  σ) - f τ¦"
  have "?N 𝟭 = (SUP τ  carrier G. 0)" using r_one by simp 
  then have "?N 𝟭 = 0" using carrier_not_empty by simp
  moreover have "?N (σ  τ)  ?N σ + ?N τ" if hστ: "σ  carrier G  τ  carrier G" for σ τ
  proof -
    have "¦f (ρ  (σ  τ)) - f ρ¦  ?N σ + ?N τ" if "ρ  carrier G" for ρ
    proof -
      have a: "¦f (ρ  (σ  τ)) - f ρ¦  ¦f (ρ  (σ  τ)) - f (ρ  σ)¦ + ¦f (ρ  σ) - f ρ¦" 
        using abs_triangle_ineq by linarith
      have "¦f (ρ  σ  τ) - f (ρ  σ)¦  ?N τ" 
        using induced_group_prenorm_welldefined[OF f_bounded] that hστ m_closed cSUP_upper by meson
      then have b: "¦f (ρ  (σ  τ)) - f (ρ  σ)¦  ?N τ" using m_assoc that hστ by simp
      have c: "¦f (ρ  σ) - f ρ¦  ?N σ" using induced_group_prenorm_welldefined[OF f_bounded] hστ that cSUP_upper by meson
      from a b c show ?thesis by argo
    qed                              
    then show ?thesis using cSUP_least carrier_not_empty by meson
  qed
  moreover have "?N (inv σ) = ?N σ" if : "σ  carrier G" for σ
  proof -
    have "¦f (τ  inv σ) - f τ¦  {¦f (ρ  σ) - f ρ¦ | ρ. ρ  carrier G }" if "τ  carrier G" for τ
    proof -
      have "¦f (τ  inv σ) - f τ¦ = ¦f (τ  inv σ) - f (τ  inv σ  σ)¦" 
        using  that m_assoc r_one l_inv by simp
      then have "¦f (τ  inv σ) - f τ¦ = ¦f (τ  inv σ  σ) - f (τ  inv σ)¦" by argo
      then show ?thesis using  that m_closed by blast
    qed
    moreover 
    have "¦f (ρ  σ) - f ρ¦  {¦f (τ  inv σ) - f τ¦ | τ. τ  carrier G }" if "ρ  carrier G" for ρ
    proof -
      have "¦f (ρ  σ) - f ρ¦ = ¦f (ρ  σ) - f (ρ  σ  inv σ)¦" 
        using  that m_assoc r_one r_inv by simp
      then have "¦f (ρ  σ) - f ρ¦ = ¦f (ρ  σ  inv σ) - f (ρ  σ)¦" by argo
      then show ?thesis using  that by blast
    qed
    ultimately have "{¦f (τ  inv σ) - f τ¦ | τ. τ  carrier G} = {¦f (ρ  σ) - f ρ¦ | ρ. ρ  carrier G}" by blast
    then show ?thesis by (simp add: setcompr_eq_image)
  qed
  ultimately show ?thesis unfolding induced_group_prenorm_def group_prenorm_def by fast
qed

lemma neighborhood_1_translation:
  assumes "neighborhood 𝟭 U" and "σ  carrier G  σ  topspace T"
  shows "neighborhood σ (σ <# U)"
proof -
  have "openin T (σ <# U)" using assms open_set_translations(1) by simp
  then show ?thesis unfolding l_coset_def using assms r_one by force
qed
           
proposition group_prenorm_continuous_if_continuous_at_1:
  assumes prenorm: "group_prenorm N" and 
    continuous_at_1: "ε>0.U. neighborhood 𝟭 U  (σU. N σ < ε)"
  shows "continuous_map T euclideanreal N"
proof -
  have "V. neighborhood σ V  (τV. N τ  Met_TC.mball (N σ) ε)" 
    if : "σ  topspace T" and : "ε > 0" for σ ε
  proof -
    from continuous_at_1 obtain U where hU: "neighborhood 𝟭 U  (τU. N τ < ε)" using  by presburger
    then have "neighborhood σ (σ <# U)" using  neighborhood_1_translation by blast
    moreover have "N (σ  τ)  Met_TC.mball (N σ) ε" if "τ  U" for τ
    proof -
      have in_group: "σ  carrier G  τ  carrier G" using  that openin_subset hU by blast
      then have "(inv σ)  (σ  τ) = τ" using l_inv l_one m_assoc inv_closed by metis
      then have "¦N (inv σ) - N (inv (σ  τ))¦  N τ" using group_prenorm_reverse_triangle_ineq 
          in_group inv_closed m_closed by (metis inv_inv prenorm)
      then have "¦N σ - N (σ  τ)¦ < ε" 
        using prenorm in_group m_closed inv_closed hU that by fastforce
      then show ?thesis unfolding Met_TC.mball_def dist_real_def by fast
    qed
    ultimately show ?thesis unfolding l_coset_def by blast
  qed
  then show ?thesis using Metric_space.continuous_map_to_metric
    by (metis Met_TC.Metric_space_axioms mtopology_is_euclidean)
qed

subsubsection ‹A prenorm respecting the group topology›

context
  fixes U :: "nat  'g set"
  assumes U_neighborhood: "n. neighborhood 𝟭 (U n)"
  assumes U_props: "n. symmetric (U n)  (U (n + 1)) <#> (U (n + 1))  (U n)"
begin

private fun V :: "nat  nat  'g set" where
"V m n = (
  if m = 0 then {} else
  if m = 1 then U n else
  if m > 2^n then carrier G else
  if even m then V (m div 2) (n - 1) else
  V ((m - 1) div 2) (n - 1) <#> U n
)"

private lemma U_in_group: "U k  carrier G" using U_neighborhood open_set_in_carrier by fast

private lemma V_in_group:
  shows "V m n  carrier G"
proof (induction n arbitrary: m)
  case (Suc n)
  then have "V ((m - 1) div 2) n <#> U (Suc n)  carrier G"
    unfolding set_mult_def using U_in_group by fast
  then show ?case using U_in_group Suc by simp
qed (auto simp: U_in_group)

private lemma V_mult:
  shows "m  1  V m n <#> U n  V (m + 1) n"
proof (induction n arbitrary: m)
  case 0
  then have "V (m + 1) 0 = carrier G" by simp
  then show ?case unfolding set_mult_def using V_in_group U_in_group by fast
next
  case (Suc n)
  then show ?case
  proof (cases "m + 1 > 2^(Suc n)")
    case True
    then have "V (m + 1) (Suc n) = carrier G" by force
    then show ?thesis unfolding set_mult_def using V_in_group U_in_group by blast
  next
    case m_in_bounds: False
    then show ?thesis
    proof (cases "m = 1")
      case True
      then show ?thesis using U_in_group U_props by force
    next
      case m_not_1: False
      then show ?thesis
      proof (cases "even m")
        case True
        then have "V m (Suc n) <#> U (Suc n) = V (m + 1) (Suc n)" using m_in_bounds m_not_1 Suc(2) by auto
        then show ?thesis by blast
      next
        case m_odd: False
        have U_mult: "U (Suc n) <#> U (Suc n)  U n" using U_props by simp 
        have not_zero: "(m - 1) div 2  1" using Suc(2) m_not_1 m_odd by presburger
        have arith: "(m - 1) div 2 + 1 = (m + 1) div 2" using Suc(2) by simp
        have "V m (Suc n) <#> U (Suc n) = V ((m - 1) div 2) n <#> U (Suc n) <#> U (Suc n)" using m_odd m_in_bounds m_not_1 Suc(2) by simp
        also have "... = V ((m - 1) div 2) n <#> (U (Suc n) <#> U (Suc n))" using set_mult_assoc V_in_group U_in_group by simp
        also have "...  V ((m - 1) div 2) n <#> U n" using mono_set_mult U_mult by blast
        also have "...  V ((m - 1) div 2 + 1) n" using Suc(1) not_zero by blast
        also have "...  = V ((m + 1) div 2) n" using arith by presburger
        also have "... =  V (m + 1) (Suc n)" using m_odd m_not_1 m_in_bounds Suc(2) by simp
        finally show ?thesis by blast
      qed
    qed
  qed
qed

private lemma V_mono:
  assumes smaller: "(real m1)/2^n1  (real m2)/2^n2" and not_zero: "m1  1  m2  1"
  shows "V m1 n1  V m2 n2"
proof -
  have "V m n  V (m + 1) n" if "m  1" for m n
  proof -
    have "V m n <#> U n  V (m + 1) n" using V_mult U_props that by presburger
    moreover have "V m n  carrier G  U n  carrier G" using U_in_group V_in_group by auto
    ultimately show ?thesis using set_mult_one_subset U_neighborhood by blast
  qed
  then have subset_suc: "V m n  V (m + 1) n" for m n by simp
  have "V m n  V (m + k) n" for m n k
  proof (induction k)
    case (Suc k)
    then show ?case unfolding Suc_eq_plus1 using subset_suc Suc
      by (metis (no_types, opaque_lifting) add.assoc dual_order.trans)
  qed (simp)
  then have a: "V m n  V m' n" if "m'  m" for m m' n using that le_Suc_ex by blast
  have b: "V m n = V (m * 2^k) (n+k)" if "m  1" for m n k
  proof (induction k)
    case (Suc k)
    have "V (m * 2^k * 2) (n + k + 1) = V (m * 2^k) (n + k)" using that by simp
    then show ?case unfolding Suc_eq_plus1 using Suc by simp
  qed (auto)
  show ?thesis
  proof (cases "n1  n2")
    case True
    have "(real m1)/2^n1 = (real (m1 * 2^(n2 - n1)))/(2^n1 * 2^(n2 - n1))" by fastforce
    also have "... = (real (m1 * 2^(n2 - n1)))/2^n2" using True by (metis le_add_diff_inverse power_add)
    finally have "(real (m1 * 2^(n2 - n1)))/2^n2  (real m2)/2^n2" using smaller by fastforce
    then have ineq: "m1 * 2^(n2 - n1)  m2"
      by (smt (verit) divide_cancel_right divide_right_mono linorder_le_cases of_nat_eq_iff of_nat_mono order_antisym_conv power_not_zero zero_le_power)
    from b have "V m1 n1 = V (m1 * 2^(n2 - n1)) (n1 + (n2 - n1))" using not_zero by blast
    also have "... = V (m1 * 2^(n2 - n1)) n2" using True by force
    finally show ?thesis using a[OF ineq] by blast
  next
    case False
    then have n2_leq_n1: "n2  n1" by simp
    have "(real m2)/2^n2 = (real (m2 * 2^(n1 - n2)))/(2^n2 * 2^(n1 - n2))" by fastforce
    also have "... = (real (m2 * 2^(n1 - n2)))/2^n1" using n2_leq_n1 by (metis le_add_diff_inverse power_add)
    finally have "(real (m2 * 2^(n1 - n2)))/2^n1  (real m1)/2^n1" using smaller by fastforce
    then have ineq: "m2 * 2^(n1 - n2)  m1"
      by (smt (verit) divide_cancel_right divide_right_mono linorder_le_cases of_nat_eq_iff of_nat_mono order_antisym_conv power_not_zero zero_le_power)
    from b have "V m2 n2 = V (m2 * 2^(n1 - n2)) (n2 + (n1 - n2))" using not_zero by blast
    also have "... = V (m2 * 2^(n1 - n2)) n1" using n2_leq_n1 by force
    finally show ?thesis using a[OF ineq] by blast
  qed
qed

private lemma approx_number_by_multiples:
  assumes hx: "x  0" and hc: "c > 0"
  shows "k :: nat  1. (real (k-1))/c  x  x < (real k)/c"
proof -
  let ?k = "x * c + 1"
  have "?k  1" using assms by simp
  moreover from this have "real (nat ?k) = ?k" by auto
  moreover have "(?k-1)/c  x  x < ?k/c" 
    using assms by (simp add: mult_imp_div_pos_le pos_less_divide_eq)
  ultimately show ?thesis
    by (smt (verit) nat_diff_distrib nat_le_eq_zle nat_one_as_int of_nat_nat)
qed

lemma construction_of_prenorm_respecting_topology:
  shows "N. group_prenorm N  
    (n. {σ  carrier G. N σ < 1/2^n}  U n)  
    (n. U n  {σ  carrier G. N σ  2/2^n})"
proof -
  define f :: "'g  real" where "f σ = Inf {(real m)/2^n | m n. σ  V m n}" for σ
  define N :: "'g  real" where "N = induced_group_prenorm f"

  have "σ  V 2 0" if "σ  carrier G" for σ using that by auto
  then have contains_2: "(real 2)/2^0  {(real m)/2^n | m n. σ  V m n}" if "σ  carrier G" for σ using that by blast
  then have nonempty: "{(real m)/2^n | m n. σ  V m n}  {}" if "σ  carrier G" for σ using that by fast
  have positive: "(real m)/2^n  0" for m n by simp
  then have bdd_below: "bdd_below {(real m)/2^n | m n. σ  V m n}" for σ by fast
  have f_bounds: "0  f σ  f σ  2" if : "σ  carrier G" for σ
  proof -
    from bdd_below have "f σ  (real 2)/2^0" unfolding f_def using cInf_lower contains_2[OF ] by meson
    moreover have "0  f σ" using cInf_greatest contains_2[OF ] unfolding f_def using positive
      by (smt (verit, del_insts) Collect_mem_eq empty_Collect_eq mem_Collect_eq)
    ultimately show ?thesis by fastforce
  qed
  then have N_welldefined: "bdd_above ((λτ. ¦f (τ  σ) - f τ¦) ` carrier G)" if "σ  carrier G" for σ
    using induced_group_prenorm_welldefined that by (metis (full_types) abs_of_nonneg)

  have in_V_if_f_smaller: "σ  V m n" if : "σ  carrier G" and smaller: "f σ < (real m)/2^n" for σ m n
  proof -
    from cInf_lessD obtain q where hq: "q  {(real m)/2^n | m n. σ  V m n}  q < (real m)/2^n"
      using smaller nonempty[OF ] unfolding f_def by (metis (mono_tags, lifting))
    then obtain m' n' where hm'n': "σ  V m' n'  q = (real m')/2^n'" by fast
    moreover have "m'  1"
    proof (rule ccontr)
      assume "¬ m'  1"
      then have "V m' n' = {}" by force
      then show "False" using hm'n' by blast
    qed
    moreover have "m  1" using f_bounds smaller 
      by (metis divide_eq_0_iff less_numeral_extra(3) less_one linorder_le_less_linear nle_le of_nat_0 order_less_imp_le)
    ultimately have "V m' n'  V m n" using V_mono hq U_props open_set_in_carrier by simp
    then show ?thesis using hm'n' by fast
  qed
  have f_1_vanishes: "f 𝟭 = 0"
  proof (rule ccontr)
    assume "f 𝟭  0"
    then have "f 𝟭 > 0" using f_bounds by fastforce
    then obtain n where hn: "f 𝟭 > (real 1)/2^n"
      by (metis divide_less_eq_1 of_nat_1 one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    have "𝟭  V 1 n" using U_neighborhood by simp
    then have "(real 1)/2^n  {(real m)/2^n |m n. 𝟭  V m n}" by fast
    then show "False" using hn cInf_lower bdd_below[of 𝟭] unfolding f_def by (smt (verit, ccfv_threshold))
  qed
  have in_U_if_N_small: "σ  U n" if in_group: "σ  carrier G" and N_small: "N σ < 1/2^n" for σ n
  proof -
    have "f σ = ¦f (𝟭  σ) - f 𝟭¦" using in_group l_one f_1_vanishes f_bounds by force
    moreover have "...  N σ" unfolding N_def induced_group_prenorm_def
      using cSUP_upper N_welldefined[OF in_group] by (metis (mono_tags, lifting) one_closed)
    ultimately have "σ  V 1 n" using in_V_if_f_smaller[OF in_group] N_small by (smt (verit) of_nat_1) 
    then show ?thesis by fastforce
  qed
  have N_bounds: "N σ  2/2^n" if : "σ  U n" for σ n
  proof -
    have diff_bounded: "f (τ  σ) - f τ  2/2^n  f (τ  inv σ) - f τ  2/2^n" if : "τ  carrier G" for τ
    proof -
      obtain k where hk: "k  1  (real (k-1))/2^n  f τ  f τ < (real k)/2^n"
        using approx_number_by_multiples[of "f τ" "2^n"] f_bounds[OF ] by auto
      then have "τ  V k n" using in_V_if_f_smaller[OF ] by blast
      moreover have "σ  V 1 n  inv σ  V 1 n" using  U_props by auto
      moreover have "V k n <#> V 1 n  V (k + 1) n"
        using V_mult U_props open_set_in_carrier hk by auto
      ultimately have "τ  σ  V (k + 1) n  τ  inv σ  V (k + 1) n" 
        unfolding set_mult_def by fast
      then have a: "(real (k + 1))/2^n  {(real m)/2^n | m n. τ  σ  V m n}
         (real (k + 1))/2^n  {(real m)/2^n | m n. τ  inv σ  V m n}" by fast
      then have "f (τ  σ)  (real (k + 1))/2^n" 
        unfolding f_def using cInf_lower[of "(real (k + 1))/2^n"] bdd_below by presburger
      moreover from a have "f (τ  inv σ)  (real (k + 1))/2^n" 
        unfolding f_def using cInf_lower[of "(real (k + 1))/2^n"] bdd_below by presburger
      ultimately show ?thesis using hk
        by (smt (verit, ccfv_SIG) diff_divide_distrib of_nat_1 of_nat_add of_nat_diff)
    qed
    have "¦f (ρ  σ) - f ρ¦  2/2^n" if : "ρ  carrier G" for ρ
    proof -
      have in_group: "σ  carrier G" using  U_in_group by fast
      then have "f (ρ  σ  inv σ) - f (ρ  σ)  2/2^n" using diff_bounded[of "ρ  σ"]  m_closed by fast
      moreover have "ρ  σ  inv σ = ρ" using m_assoc r_inv r_one in_group inv_closed  by presburger
      ultimately have "f ρ - f (ρ  σ)  2/2^n" by force
      moreover have "f (ρ  σ) - f ρ  2/2^n" using diff_bounded[OF ] by fast
      ultimately show ?thesis by force
    qed
    then show ?thesis unfolding N_def induced_group_prenorm_def using cSUP_least carrier_not_empty by meson
  qed
  then have "U n  {σ  carrier G. N σ  2/2^n}" for n using U_in_group by blast
  moreover have "group_prenorm N" unfolding N_def 
    using bounded_function_induces_group_prenorm f_bounds by (metis abs_of_nonneg)
  ultimately show ?thesis using in_U_if_N_small by blast
qed
end

subsubsection ‹Proof of Birkhoff-Kakutani›

lemma first_countable_neighborhoods_of_1_sequence:
  assumes "first_countable T"
  shows "U :: nat  'g set. 
    (n. neighborhood 𝟭 (U n)  symmetric (U n)  U (n + 1) <#> U (n + 1)  U n)  
    (W. neighborhood 𝟭 W  (n. U n  W))"
proof -
  from assms obtain  where hℬ: 
    "countable   (W. openin T W)  (U. neighborhood 𝟭 U  (W. 𝟭  W  W  U))"
    unfolding first_countable_def by fastforce
  define 𝔅 :: "'g set set" where "𝔅 = insert (carrier G) {W  . 𝟭  W}"
  define B :: "nat  'g set" where "B = from_nat_into 𝔅"
  have "𝔅  {}  (W𝔅. neighborhood 𝟭 W)" unfolding 𝔅_def using hℬ
    by (metis group_is_space insert_iff insert_not_empty mem_Collect_eq one_closed openin_topspace)
  then have B_neighborhood: "n. neighborhood 𝟭 (B n)" unfolding B_def by (simp add: from_nat_into)
  define P where "P n V  V  B n  neighborhood 𝟭 V  symmetric V" for n V
  define Q where "Q (n :: nat) V W  W <#> W  V" for n V W
  have "V. P 0 V"
  proof -
    obtain W where "neighborhood 𝟭 W  symmetric W  W <#> W  B 0" 
      using neighborhoods_of_1 B_neighborhood by fastforce
    moreover from this have "W  B 0" using set_mult_one_subset open_set_in_carrier by blast
    ultimately show ?thesis unfolding P_def by auto
  qed
  moreover have "W. P (Suc n) W  Q n V W" if "P n V" for n V
  proof -
    have "neighborhood 𝟭 (V  B (Suc n))" using B_neighborhood that unfolding P_def by auto
    then obtain W where "neighborhood 𝟭 W  symmetric W  W <#> W  V  B (Suc n)" 
      using neighborhoods_of_1 by fastforce
    moreover from this have "W  B (Suc n)" 
      using set_mult_one_subset[of W W] open_set_in_carrier[of W] by fast
    ultimately show ?thesis unfolding P_def Q_def by auto
  qed
  ultimately obtain U where hU: "n. P n (U n)  Q n (U n) (U (Suc n))"
    using dependent_nat_choice by metis
  moreover have "n. U n  W" if "neighborhood 𝟭 W" for W
  proof -
    from that obtain W' where hW': "W'    𝟭  W'  W'  W" using hℬ by blast
    then have "W'  𝔅  countable 𝔅" unfolding 𝔅_def using hℬ by simp
    then obtain n where "B n = W'" unfolding B_def using from_nat_into_to_nat_on by fast
    then show ?thesis using hW' hU unfolding P_def by blast
  qed
  ultimately show ?thesis unfolding P_def Q_def by auto
qed

definition "left_invariant_metric Δ  Metric_space (carrier G) Δ 
  (σ τ ρ. σ  carrier G  τ  carrier G  ρ  carrier G  Δ (ρ  σ) (ρ  τ) = Δ σ τ)"

definition "right_invariant_metric Δ  Metric_space (carrier G) Δ 
  (σ τ ρ. σ  carrier G  τ  carrier G  ρ  carrier G  Δ (σ  ρ) (τ  ρ) = Δ σ τ)"

lemma left_invariant_metricE:
  assumes "left_invariant_metric Δ" "σ  carrier G" "τ  carrier G" "ρ  carrier G"
  shows "Δ (ρ  σ) (ρ  τ) = Δ σ τ"
  using assms unfolding left_invariant_metric_def by blast

lemma right_invariant_metricE:
  assumes "right_invariant_metric Δ" "σ  carrier G" "τ  carrier G" "ρ  carrier G"
  shows "Δ (σ  ρ) (τ  ρ) = Δ σ τ"
  using assms unfolding right_invariant_metric_def by blast

theorem Birkhoff_Kakutani_left:
  assumes Hausdorff: "Hausdorff_space T" and first_countable: "first_countable T"
  shows "Δ. left_invariant_metric Δ  Metric_space.mtopology (carrier G) Δ = T"
proof -
  from first_countable obtain U :: "nat  'g set" where 
    U_props: "n. neighborhood 𝟭 (U n)  symmetric (U n)  U (n + 1) <#> U (n + 1)  U n" and
    neighborhood_base: "W. neighborhood 𝟭 W  (n. U n  W)"
    using first_countable_neighborhoods_of_1_sequence by auto
  from U_props obtain N where
    prenorm: "group_prenorm N" and
    norm_ball_in_U: "n. {σ  carrier G. N σ < 1/2^n}  U n" and
    U_in_norm_ball: "n. U n  {σ  carrier G. N σ  2/2^n}"
    using construction_of_prenorm_respecting_topology by meson
  have continuous: "continuous_map T euclideanreal N" using prenorm
  proof (rule group_prenorm_continuous_if_continuous_at_1, intro allI impI)
    fix ε :: real assume "ε > 0"
    then obtain n where hn: "1/2^n < ε" 
      by (metis divide_less_eq_1_pos one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    then have "N σ < ε" if "σ  U (n + 1)" for σ using that U_in_norm_ball by fastforce
    then show "U. neighborhood 𝟭 U  (σU. N σ < ε)" using U_props by meson
  qed
  let ?B = "λε. {σ  carrier G. N σ < ε}"
  let  = "λσ τ. N (inv σ  τ)"
  let  = "λσ τ. if σ  carrier G  τ  carrier G then  σ τ else 42"
  have " σ τ  0" if "σ  carrier G  τ  carrier G" for σ τ
    using group_prenorm_nonnegative prenorm that by blast
  moreover have " σ τ =  τ σ" if "σ  carrier G  τ  carrier G" for σ τ
  proof -
    have "inv τ  σ = inv (inv σ  τ)" using inv_mult_group inv_inv that by auto
    then show ?thesis using prenorm that by fastforce
  qed
  moreover have " σ τ = 0  σ = τ" if "σ  carrier G  τ  carrier G" for σ τ
  proof
    assume " σ τ = 0"
    then have "inv σ  τ  U n" for n using norm_ball_in_U that by fastforce
    then have "inv σ  τ  W" if "neighborhood 𝟭 W" for W using neighborhood_base that by auto
    then have "inv σ  τ = 𝟭" using Hausdorff_space_sing_Inter_opens[of T 𝟭] Hausdorff by blast
    then show "σ = τ" using inv_comm inv_equality that by fastforce
  next
    assume "σ = τ"
    then show " σ τ = 0" using that prenorm by force
  qed
  moreover have " σ ρ   σ τ +  τ ρ" if "σ  carrier G  τ  carrier G  ρ  carrier G" for σ τ ρ
  proof -
    have "inv σ  ρ = (inv σ  τ)  (inv τ  ρ)" using m_assoc[symmetric] that by (simp add: inv_solve_right)
    then show ?thesis using prenorm that by auto
  qed                        
  ultimately have metric: "Metric_space (carrier G) " unfolding Metric_space_def by auto
  then interpret Metric_space "carrier G"  by blast
  have " (ρ  σ) (ρ  τ) =  σ τ" if "σ  carrier G  τ  carrier G  ρ  carrier G" for σ τ ρ
  proof -
    have "inv σ  τ = inv (ρ  σ)  (ρ  τ)" using that m_assoc[symmetric] by (simp add: inv_solve_left inv_solve_right)
    then show ?thesis by simp
  qed
  then have left_invariant: "left_invariant_metric " 
    unfolding left_invariant_metric_def using metric by auto
  have mball_coset_of_norm_ball: "mball σ ε = σ <# ?B ε" if : "σ  carrier G" for σ ε
  proof -
    have "mball σ ε = {τ  carrier G. N (inv σ  τ) < ε}" unfolding mball_def using  by auto
    also have "... = σ <# (?B ε)"
    proof -
      have "τ  σ <# (?B ε)" if "τ  carrier G  N (inv σ  τ) < ε" for τ
      proof -
        have "σ  (inv σ  τ) = τ" using  that by (metis inv_closed inv_solve_left m_closed)
        moreover have "inv σ  τ  ?B ε" using  that by fastforce
        ultimately show ?thesis unfolding l_coset_def by force
      qed
      moreover have "τ  carrier G  N (inv σ  τ) < ε" if "τ  σ <# (?B ε)" for τ
      proof -
        from that obtain ρ where "ρ  ?B ε  τ = σ  ρ" unfolding l_coset_def by blast
        moreover from this have "inv σ  τ = ρ" using  by (simp add: inv_solve_left')
        ultimately show ?thesis using  by simp
      qed
      ultimately show ?thesis by blast
    qed
    finally show ?thesis by presburger
  qed
  define ball where "ball S  (σ ε. σ  carrier G  S = mball σ ε)" for S
  have "openin mtopology V" if "ball V" for V using that unfolding ball_def by fast
  moreover have "W. ball W  σ  W  W  V" if "openin mtopology V  σ  V" for σ V
    unfolding ball_def using openin_mtopology that by (smt (verit, best) centre_in_mball_iff subset_iff)
  ultimately have openin_metric: "openin mtopology = arbitrary union_of ball" 
    by (simp add: openin_topology_base_unique)
  have "openin T V" if "ball V" for V
  proof -
    from that obtain σ ε where "σ  carrier G  V = σ <# ?B ε" 
      unfolding ball_def using mball_coset_of_norm_ball by blast
    moreover have "openin T (?B ε)" using continuous
      by (simp add: continuous_map_upper_lower_semicontinuous_lt)
    ultimately show ?thesis using open_set_translations(1) by presburger
  qed
  moreover have "W. ball W  σ  W  W  V" if "neighborhood σ V" for σ V
  proof -
    from that have in_group: "σ  carrier G" using open_set_in_carrier by fast
    then have "neighborhood 𝟭 (inv σ <# V)" 
      using l_coset_def open_set_translations(1) that l_inv by fastforce
    then obtain n where "U n  inv σ <# V" using neighborhood_base by presburger
    then have "?B (1/2^n)  inv σ <# V" using norm_ball_in_U by blast
    then have "σ <# ?B (1/2^n)  σ <# (inv σ <# V)" unfolding l_coset_def by fast
    also have "... = V" using in_group that open_set_in_carrier by (simp add: lcos_m_assoc lcos_mult_one)
    finally have "mball σ (1/2^n)  V" using mball_coset_of_norm_ball in_group by blast
    then show ?thesis unfolding ball_def
      by (smt (verit) centre_in_mball_iff divide_pos_pos in_group one_add_one zero_less_power zero_less_two)
  qed
  ultimately have "openin T = arbitrary union_of ball" by (simp add: openin_topology_base_unique)
  then show ?thesis using left_invariant openin_metric topology_eq by fastforce
qed

theorem Birkhoff_Kakutani_right:
  assumes Hausdorff: "Hausdorff_space T" and first_countable: "first_countable T"
  shows "Δ. right_invariant_metric Δ  Metric_space.mtopology (carrier G) Δ = T"
proof -
  from first_countable obtain U :: "nat  'g set" where 
    U_props: "n. neighborhood 𝟭 (U n)  symmetric (U n)  U (n + 1) <#> U (n + 1)  U n" and
    neighborhood_base: "W. neighborhood 𝟭 W  (n. U n  W)"
    using first_countable_neighborhoods_of_1_sequence by auto
  from U_props obtain N where
    prenorm: "group_prenorm N" and
    norm_ball_in_U: "n. {σ  carrier G. N σ < 1/2^n}  U n" and
    U_in_norm_ball: "n. U n  {σ  carrier G. N σ  2/2^n}"
    using construction_of_prenorm_respecting_topology by meson
  have continuous: "continuous_map T euclideanreal N" using prenorm
  proof (rule group_prenorm_continuous_if_continuous_at_1, intro allI impI)
    fix ε :: real assume "ε > 0"
    then obtain n where hn: "1/2^n < ε" 
      by (metis divide_less_eq_1_pos one_less_numeral_iff power_one_over real_arch_pow_inv semiring_norm(76) zero_less_numeral)
    then have "N σ < ε" if "σ  U (n + 1)" for σ using that U_in_norm_ball by fastforce
    then show "U. neighborhood 𝟭 U  (σU. N σ < ε)" using U_props by meson
  qed
  let ?B = "λε. {σ  carrier G. N σ < ε}"
  let  = "λσ τ. N (σ  inv τ)"
  let  = "λσ τ. if σ  carrier G  τ  carrier G then  σ τ else 42"
  have " σ τ  0" if "σ  carrier G  τ  carrier G" for σ τ
    using group_prenorm_nonnegative prenorm that by blast
  moreover have " σ τ =  τ σ" if "σ  carrier G  τ  carrier G" for σ τ
  proof -
    have "τ  inv σ = inv (σ  inv τ)" using inv_mult_group inv_inv that by auto
    then show ?thesis using prenorm that by auto 
  qed
  moreover have " σ τ = 0  σ = τ" if "σ  carrier G  τ  carrier G" for σ τ
  proof
    assume " σ τ = 0"
    then have "σ  inv τ  U n" for n using norm_ball_in_U that by fastforce
    then have "σ  inv τ  W" if "neighborhood 𝟭 W" for W using neighborhood_base that by auto
    then have "σ  inv τ = 𝟭" using Hausdorff_space_sing_Inter_opens[of T 𝟭] Hausdorff by blast
    then show "σ = τ" using inv_equality that by fastforce
  next
    assume "σ = τ"
    then show " σ τ = 0" using that prenorm by force
  qed
  moreover have " σ ρ   σ τ +  τ ρ" if "σ  carrier G  τ  carrier G  ρ  carrier G" for σ τ ρ
  proof -
    have "σ  inv ρ = (σ  inv τ)  (τ  inv ρ)" using m_assoc that by (simp add: inv_solve_left)
    then show ?thesis using prenorm that by auto
  qed                        
  ultimately have metric: "Metric_space (carrier G) " unfolding Metric_space_def by auto
  then interpret Metric_space "carrier G"  by blast
  have " (σ  ρ) (τ  ρ) =  σ τ" if "σ  carrier G  τ  carrier G  ρ  carrier G" for σ τ ρ
  proof -
    have "σ  inv τ = (σ  ρ)  inv (τ  ρ)" using that m_assoc by (simp add: inv_solve_left inv_solve_right)
    then show ?thesis by simp
  qed
  then have right_invariant: "right_invariant_metric " 
    unfolding right_invariant_metric_def using metric by auto
  have mball_coset_of_norm_ball: "mball σ ε = ?B ε #> σ" if : "σ  carrier G" for σ ε
  proof -
    have "mball σ ε = {τ  carrier G. N (σ  inv τ) < ε}" unfolding mball_def using  by auto
    also have "... = (?B ε) #> σ"
    proof -
      have "τ  (?B ε) #> σ" if "τ  carrier G  N (σ  inv τ) < ε" for τ
      proof -
        have "inv (σ  inv τ)  σ = τ" using  that by (simp add: inv_mult_group m_assoc)
        moreover have "inv (σ  inv τ)  ?B ε" using  that prenorm by fastforce
        ultimately show ?thesis unfolding r_coset_def by force
      qed
      moreover have "τ  carrier G  N (σ  inv τ) < ε" if "τ  (?B ε) #> σ" for τ
      proof -
        from that obtain ρ where "ρ  ?B ε  τ = ρ  σ" unfolding r_coset_def by blast
        moreover from this have "σ  inv τ = inv ρ" using 
          by (metis (no_types, lifting) inv_closed inv_mult_group inv_solve_left m_closed mem_Collect_eq)
        ultimately show ?thesis using  prenorm by fastforce
      qed
      ultimately show ?thesis by blast
    qed
    finally show ?thesis by presburger
  qed
  define ball where "ball S  (σ ε. σ  carrier G  S = mball σ ε)" for S
  have "openin mtopology V" if "ball V" for V using that unfolding ball_def by fast
  moreover have "W. ball W  σ  W  W  V" if "openin mtopology V  σ  V" for σ V
    unfolding ball_def using openin_mtopology that by (smt (verit, best) centre_in_mball_iff subset_iff)
  ultimately have openin_metric: "openin mtopology = arbitrary union_of ball" 
    by (simp add: openin_topology_base_unique)
  have "openin T V" if "ball V" for V
  proof -
    from that obtain σ ε where "σ  carrier G  V = ?B ε #> σ" 
      unfolding ball_def using mball_coset_of_norm_ball by blast
    moreover have "openin T (?B ε)" using continuous
      by (simp add: continuous_map_upper_lower_semicontinuous_lt)
    ultimately show ?thesis using open_set_translations(2) by presburger
  qed
  moreover have "W. ball W  σ  W  W  V" if "neighborhood σ V" for σ V
  proof -
    from that have in_group: "σ  carrier G" using open_set_in_carrier by fast
    then have "neighborhood 𝟭 (V #> inv σ)" 
      using r_coset_def open_set_translations(2) that r_inv by fastforce
    then obtain n where "U n  V #> inv σ" using neighborhood_base by presburger
    then have "?B (1/2^n)  V #> inv σ" using norm_ball_in_U by blast
    then have "?B (1/2^n) #> σ  (V #> inv σ) #> σ" unfolding r_coset_def by fast
    also have "...  = V" using in_group that open_set_in_carrier by (simp add: coset_mult_assoc)
    finally have "mball σ (1/2^n)  V" using mball_coset_of_norm_ball in_group by blast
    then show ?thesis unfolding ball_def
      by (smt (verit) centre_in_mball_iff divide_pos_pos in_group one_add_one zero_less_power zero_less_two)
  qed
  ultimately have "openin T = arbitrary union_of ball" by (simp add: openin_topology_base_unique)
  then show ?thesis using right_invariant openin_metric topology_eq by fastforce
qed                                     

corollary Birkhoff_Kakutani_iff:
  shows "metrizable_space T  Hausdorff_space T  first_countable T"
  using Birkhoff_Kakutani_left Metric_space.metrizable_space_mtopology metrizable_imp_Hausdorff_space 
    metrizable_imp_first_countable unfolding left_invariant_metric_def by metis

end

end