mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers

English

For any x,y ∈ G, MapClusterPt x atTop (y^·:ℕ→G) holds if and only if x belongs to the topological closure of the subgroup generated by y as powers (zpowers).

Русский

Для любых x,y ∈ G, утверждение MapClusterPt x atTop (y^·:ℕ→G) эквивалентно тому, что x лежит в топологическом замыкании zpowers(y).

LaTeX

$$$\\operatorname{MapClusterPt}(x,\\mathrm{atTop}, y^{\\cdot}) \ \Longleftrightarrow \ x \\in (\\operatorname{zpowers}(y)).topologicalClosure$$$

Lean4

@[to_additive]
theorem mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers {x y : G} :
    MapClusterPt x atTop (y ^ · : ℕ → G) ↔ x ∈ (Subgroup.zpowers y).topologicalClosure :=
  (mapClusterPt_atTop_pow_tfae x y).out 0 3

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