instUniformContinuousConstSMul — Mathlib

English

The action by M on the completion is uniformly continuous with constant-smul: there is a UniformContinuousConstSMul action on Completion X.

Русский

Действие множителя M на дополнение обладает равномерной непрерывностью константного умножения: существует равномерно непрерывное действие на Completion X.

LaTeX

$$$\\langle \\text{UniformContinuousConstSMul } M\\; (\\mathrm{Completion}(X)) \\rangle$$$

Lean4

@[to_additive]
instance : UniformContinuousConstSMul M (Completion X) :=
  ⟨fun _ => uniformContinuous_map⟩

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