exists_pow_mem_of_mem_nhds — Mathlib

English

Same content as above: existence of a^n in given nhds neighborhood of 0 for a topologically nilpotent element.

Русский

То же самое: существование a^n в заданной окрестности 0 для топологически нильпотентного элемента.

LaTeX

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

Lean4

theorem exists_pow_mem_of_mem_nhds {a : R} (ha : IsTopologicallyNilpotent a) {v : Set R} (hv : v ∈ 𝓝 0) :
    ∃ n, a ^ n ∈ v :=
  (ha.eventually_mem hv).exists

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