English
For any x ∈ G and integer m, x^m is a cluster point of the sequence x^n as n → ∞ (i.e., MapClusterPt (x^m) atTop (x^·)).
Русский
Для любого x ∈ G и целого m, элемент x^m является кластерной точкой последовательности x^n при n → ∞ (то есть MapClusterPt(x^m) atTop (x^·)).
LaTeX
$$$\forall x\in G,\ \forall m\in\mathbb{Z},\; MapClusterPt(x^{m})\;\text{atTop}\; (x^{\cdot})$$$
Lean4
@[to_additive]
theorem mapClusterPt_self_zpow_atTop_pow (x : G) (m : ℤ) : MapClusterPt (x ^ m) atTop (x ^ · : ℕ → G) :=
by
obtain ⟨y, hy⟩ : ∃ y, MapClusterPt y atTop (x ^ · : ℤ → G) := exists_clusterPt_of_compactSpace _
rw [← mapClusterPt_atTop_zpow_iff_pow]
have H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿(fun a b ↦ x ^ (m + b - a)) :=
by
have : ContinuousAt (fun yz ↦ x ^ m * yz.2 / yz.1) (y, y) := by fun_prop
simpa only [comp_def, ← zpow_sub, ← zpow_add, div_eq_mul_inv, Prod.map, mul_inv_cancel_right] using
(hy.curry_prodMap hy).continuousAt_comp this
suffices Tendsto ↿(fun a b ↦ m + b - a) (atTop.curry atTop) atTop from H.of_comp this
refine Tendsto.curry <| .of_forall fun a ↦ ?_
simp only [sub_eq_add_neg] -- TODO: add `Tendsto.atTop_sub_const` etc
exact tendsto_atTop_add_const_right _ _ (tendsto_atTop_add_const_left atTop m tendsto_id)
