English
For a group M acting on a uniform space X with a uniform continuous constant-smul, if c is a unit in M, then c acts trivially on the uniformity: c • 𝓤 X = 𝓤 X.
Русский
Для группы M, действующей на равномерном пространстве X с равномерно непрерывным постоянным умножением, если c — единица, то c действует trivially на униформности: c • 𝓤 X = 𝓤 X.
LaTeX
$$$\\forall c \\in M,\\; \\text{IsUnit}(c) \\Rightarrow c \\cdot \\mathcal{U} X = \\mathcal{U} X$$$
Lean4
@[to_additive]
theorem smul_uniformity [Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] {c : M} (hc : IsUnit c) :
c • 𝓤 X = 𝓤 X :=
let ⟨d, hcd⟩ := hc.exists_right_inv
have cU : c • 𝓤 X ≤ 𝓤 X := uniformContinuous_const_smul c
have dU : d • 𝓤 X ≤ 𝓤 X := uniformContinuous_const_smul d
le_antisymm cU <| by simpa [smul_smul, hcd] using Filter.smul_filter_le_smul_filter (a := c) dU
