smul_uniformity — Mathlib

English

Let M be a group acting on X with uniform continuous constant smul. Then for any c ∈ M, c • 𝓤 X = 𝓤 X.

Русский

Пусть M действует на X с равномерно непрерывным константным умножением. Тогда для любого c ∈ M выполняется c • 𝓤 X = 𝓤 X.

LaTeX

$$$\\forall c \\in M,\\; c \\cdot \\mathcal{U} X = \\mathcal{U} X$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_uniformity [Group M] [MulAction M X] [UniformContinuousConstSMul M X] (c : M) : c • 𝓤 X = 𝓤 X :=
  Group.isUnit _ |>.smul_uniformity

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