smul_uniformity₀ — Mathlib

English

If M is a GroupWithZero acting on X with UniformContinuousConstSMul and c ≠ 0, then c • 𝓤 X = 𝓤 X.

Русский

Пусть M — группа с нулём, действующая на X с равномерно непрерывным константным умножением, и c ≠ 0. Тогда c • 𝓤 X = 𝓤 X.

LaTeX

$$$\\forall c \\in M,\\; (c \\neq 0) \\Rightarrow c \\cdot \\mathcal{U} X = \\mathcal{U} X$$$

Lean4

theorem smul_uniformity₀ [GroupWithZero M] [MulAction M X] [UniformContinuousConstSMul M X] {c : M} (hc : c ≠ 0) :
    c • 𝓤 X = 𝓤 X :=
  hc.isUnit.smul_uniformity

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