mul_right_of_commute — Mathlib

English

Locally finite of multiplicative supports yields a Finset controlling the supports near x.

Русский

Локальная конечность мультиподдержек дает конечный набор индексов, управляющий поддержками рядом с x.

LaTeX

$$$\exists \text{is} : \Finset ι,\ \exists n \in 𝓝 x,\ n \subseteq \bigcap_{i\in \text{is}} U_i \land \forall z \in n,\ \operatorname{mulSupport}(\lambda i. f_i(z)) \subseteq \text{is}.$$$

Lean4

/-- If `a` and `b` commute and `a` is topologically nilpotent,
  then `a * b` is topologically nilpotent. -/
theorem mul_right_of_commute [IsLinearTopology Rᵐᵒᵖ R] {a b : R} (ha : IsTopologicallyNilpotent a) (hab : Commute a b) :
    IsTopologicallyNilpotent (a * b) :=
  by
  simp_rw [IsTopologicallyNilpotent, hab.mul_pow]
  exact IsLinearTopology.tendsto_mul_zero_of_left _ _ ha

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