add — Mathlib

English

If a and b are topologically nilpotent and commute, then a + b is topologically nilpotent.

Русский

Если a и b топологически нильпотентны и commute, то a + b топологически нильпотентен.

LaTeX

$$$\text{IsTopologicallyNilpotent}(a) \land \text{IsTopologicallyNilpotent}(b) \land [a,b]=0 \Rightarrow \text{IsTopologicallyNilpotent}(a+b).$$$

Lean4

/-- If `a` and `b` are topologically nilpotent, then `a + b` is topologically nilpotent. -/
theorem add {a b : R} (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) :
    IsTopologicallyNilpotent (a + b) :=
  ha.add_of_commute hb (Commute.all ..)

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