English
There is a four-way equivalence (TFAE) among: (i) MapClusterPt x atTop (y^· : ℕ → G); (ii) MapClusterPt x atTop (y^· : ℤ → G); (iii) x ∈ closure(range (y^· : ℕ → G)); (iv) x ∈ closure(range (y^· : ℤ → G)).
Русский
Существует четырехчленный цикл эквивалентности (TFAE) между: (i) MapClusterPt x atTop (y^·: ℕ → G); (ii) MapClusterPt x atTop (y^·: ℤ → G); (iii) x ∈ замыкание диапазона (y^· : ℕ → G); (iv) x ∈ замыкание диапазона (y^· : ℤ → G).
LaTeX
$$$\text{P}_1 \iff \text{P}_2$, $\text{P}_1 \iff \text{P}_3$, $\text{P}_1 \iff \text{P}_4$, where$\;\begin{aligned} \text{P}_1 &:= \text{MapClusterPt}(x,\mathrm{atTop}, y^\cdot:\mathbb{N}\to G), \\ \text{P}_2 &:= \text{MapClusterPt}(x,\mathrm{atTop}, y^\cdot:\mathbb{Z}\to G), \\ \text{P}_3 &:= x \in \overline{\{y^n:n\in\mathbb{N}\}}, \\ \text{P}_4 &:= x \in \overline{\{y^n:n\in\mathbb{Z}\}}. \end{aligned}$$$
Lean4
@[to_additive]
theorem mapClusterPt_atTop_zpow_iff_pow [DivInvMonoid G] [TopologicalSpace G] {x y : G} :
MapClusterPt x atTop (y ^ · : ℤ → G) ↔ MapClusterPt x atTop (y ^ · : ℕ → G) := by
simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]
