mapClusterPt_self_atTop_pow — Mathlib

English

For any x ∈ G, x is a cluster point of the sequence x^n as n → ∞, i.e., MapClusterPt x atTop (x^· : ℕ → G).

Русский

Для любого x ∈ G, сама x является кластерной точкой последовательности x^n при n → ∞.

LaTeX

$$$\text{MapClusterPt}(x,\mathrm{atTop}, (x^{\cdot}:\mathbb{N}\to G))$$$

Lean4

@[to_additive]
theorem mapClusterPt_self_atTop_pow (x : G) : MapClusterPt x atTop (x ^ · : ℕ → G) := by
  simpa using mapClusterPt_self_zpow_atTop_pow x 1

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