isTopologicallyNilpotent — Mathlib

English

If a is topologically nilpotent, then for every nhds neighborhood of 0 there exists an n with a^n in that neighborhood.

Русский

Если a топологически нильпотентен, то для любой окрестности 0 существует n такое, что a^n лежит в этой окрестности.

LaTeX

$$$\text{IsTopologicallyNilpotent}(a) \Rightarrow \forall v \ni 0, \exists n, a^n \in v.$$$

Lean4

theorem _root_.IsNilpotent.isTopologicallyNilpotent {a : R} (ha : IsNilpotent a) : IsTopologicallyNilpotent a :=
  by
  obtain ⟨n, hn⟩ := ha
  apply tendsto_atTop_of_eventually_const (i₀ := n)
  intro i hi
  rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]

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