Documentation

Mathlib.Topology.Algebra.Group.SubmonoidClosure

Topological closure of the submonoid closure #

In this file we prove several versions of the following statement: if G is a compact topological group and s : Set G, then the topological closures of Submonoid.closure s and Subgroup.closure s are equal.

The proof is based on the following observation, see mapClusterPt_self_zpow_atTop_pow: each x^m, m : ℤ is a limit point (MapClusterPt) of the sequence x^n, n : ℕ, as n → ∞.

theorem closure_range_zpow_eq_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [TopologicalGroup G] (x : G) :
closure (Set.range fun (x_1 : ) => x ^ x_1) = closure (Set.range fun (x_1 : ) => x ^ x_1)
theorem denseRange_zpow_iff_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [TopologicalGroup G] {x : G} :
(DenseRange fun (x_1 : ) => x ^ x_1) DenseRange fun (x_1 : ) => x ^ x_1
theorem denseRange_zsmul_iff_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [TopologicalAddGroup G] {x : G} :
(DenseRange fun (x_1 : ) => x_1 x) DenseRange fun (x_1 : ) => x_1 x