English
The four-way equivalence among: MapClusterPt x atTop (y^·:ℕ→G), MapClusterPt x atTop (y^·:ℤ→G), x ∈ closure (range (y^·:ℕ→G)), x ∈ closure (range (y^·:ℤ→G)).
Русский
Четыре взаимно эквивалентных утверждения между: ClusterPt, соответствующий по AtTop, и замыкания диапазонов степеней y.
LaTeX
$$$(\text{P}_1 \iff \text{P}_2) \land (\text{P}_1 \iff \text{P}_3) \land (\text{P}_1 \iff \text{P}_4)$, где $\text{P}_1 := \text{MapClusterPt}(x,\mathrm{atTop}, y^\cdot)$, $\text{P}_2 := \text{MapClusterPt}(x,\mathrm{atTop}, y^\cdot)$, $\text{P}_3 := x \in \overline{\mathrm{range}(y^\cdot:\mathbb{N}\to G)}$, $\text{P}_4 := x \in \overline{\mathrm{range}(y^\cdot:\mathbb{Z}\to G)}.$$$
Lean4
@[to_additive]
theorem mapClusterPt_atTop_pow_tfae (x y : G) :
List.TFAE
[MapClusterPt x atTop (y ^ · : ℕ → G), MapClusterPt x atTop (y ^ · : ℤ → G), x ∈ closure (range (y ^ · : ℕ → G)),
x ∈ closure (range (y ^ · : ℤ → G)), ] :=
by
tfae_have 2 ↔ 1 := mapClusterPt_atTop_zpow_iff_pow
tfae_have 3 → 4 := by
refine fun h ↦ closure_mono (range_subset_iff.2 fun n ↦ ?_) h
exact ⟨n, zpow_natCast _ _⟩
tfae_have 4 → 1 := by
refine fun h ↦ closure_minimal ?_ isClosed_setOf_clusterPt h
exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _)
tfae_have 1 → 3 := by
rw [mem_closure_iff_clusterPt]
exact (ClusterPt.mono · (le_principal_iff.2 range_mem_map))
tfae_finish
