IsTopologicallyNilpotent — Mathlib

English

An element a of a topological monoid is topologically nilpotent if its powers tend to zero in the topology.

Русский

Элемент a полугруппы с топологией является топологически нильпотентным, если её степени a^n стремятся к нулю в данной топологии.

LaTeX

$$$a \text{ is topologically nilpotent} \iff \lim_{n\to\infty} a^n = 0 \text{ in the topology}.$$$

Lean4

/-- An element is topologically nilpotent if its powers converge to `0`. -/
def IsTopologicallyNilpotent {R : Type*} [MonoidWithZero R] [TopologicalSpace R] (a : R) : Prop :=
  Tendsto (a ^ ·) atTop (𝓝 0)

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