closure_range_zpow_eq_pow — Mathlib

English

For any set s ⊆ G, the topological closure of the subgroup closure of s equals the topological closure of the submonoid closure of s.

Русский

Для любого набора s ⊆ G верхнее топологическое замыкание закрытия подгруппы от s равно верхнему топологическому замыканию закрытия субмоноида от s.

LaTeX

$$$\operatorname{topologicalClosure}((\operatorname{closure}_{\mathrm{Subgroup}}(s))) = \operatorname{topologicalClosure}((\operatorname{closure}_{\mathrm{Submonoid}}(s))).$$$

Lean4

@[to_additive]
theorem closure_range_zpow_eq_pow (x : G) : closure (range (x ^ · : ℤ → G)) = closure (range (x ^ · : ℕ → G)) :=
  by
  ext y
  exact (mapClusterPt_atTop_pow_tfae y x).out 3 2

Похожие утверждения