to_continuousConstSMul — Mathlib

English

If M with a uniform continuous smul structure acts on X, then this induces a continuous constant smul structure on X.

Русский

Если M действует на X посредством равномерно непрерывного умножения, то это порождает непрерывное константное умножение на X.

LaTeX

$$$\text{to\_continuousConstSMul}$$$

Lean4

@[to_additive]
instance (priority := 100) to_continuousConstSMul [UniformContinuousConstSMul M X] : ContinuousConstSMul M X :=
  ⟨fun c => (uniformContinuous_const_smul c).continuous⟩

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