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
mapClusterPt_self_zpow_atTop_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
(x : G)
(m : ℤ)
:
MapClusterPt (x ^ m) Filter.atTop fun (x_1 : ℕ) => x ^ x_1
theorem
mapClusterPt_self_zsmul_atTop_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
(x : G)
(m : ℤ)
:
MapClusterPt (m • x) Filter.atTop fun (x_1 : ℕ) => x_1 • x
theorem
mapClusterPt_one_atTop_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
(x : G)
:
MapClusterPt 1 Filter.atTop fun (x_1 : ℕ) => x ^ x_1
theorem
mapClusterPt_zero_atTop_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
(x : G)
:
MapClusterPt 0 Filter.atTop fun (x_1 : ℕ) => x_1 • x
theorem
mapClusterPt_self_atTop_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
(x : G)
:
MapClusterPt x Filter.atTop fun (x_1 : ℕ) => x ^ x_1
theorem
mapClusterPt_self_atTop_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
(x : G)
:
MapClusterPt x Filter.atTop fun (x_1 : ℕ) => x_1 • x
theorem
mapClusterPt_atTop_pow_tfae
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
(x y : G)
:
theorem
mapClusterPt_atTop_nsmul_tfae
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
(x y : G)
:
@[simp]
theorem
mapClusterPt_inv_atTop_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
{x y : G}
:
(MapClusterPt x⁻¹ Filter.atTop fun (x : ℕ) => y ^ x) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => y ^ x
@[simp]
theorem
mapClusterPt_neg_atTop_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
{x y : G}
:
(MapClusterPt (-x) Filter.atTop fun (x : ℕ) => x • y) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => x • y
theorem
closure_range_zpow_eq_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
(x : G)
:
theorem
closure_range_zsmul_eq_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
(x : G)
:
theorem
denseRange_zpow_iff_pow
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalGroup G]
{x : G}
:
theorem
denseRange_zsmul_iff_nsmul
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[CompactSpace G]
[TopologicalAddGroup G]
{x : G}
: