uniformContinuousConstSMul — Mathlib

English

If M, α, X form a suitable setting with a uniform continuous constant scalar multiplication, then UniformFun α X inherits UniformContinuousConstSMul M X; i.e., uniform continuity of constant smul carries over to UniformFun.

Русский

Если имеется подходящая структура для константного умножения, то UniformFun α X наследует UniformContinuousConstSMul M X.

LaTeX

$$$UniformContinuousConstSMul\; M\; X \Rightarrow UniformContinuousConstSMul\; M\; (\mathrm{UniformFun} \; α \; X).$$$

Lean4

instance uniformContinuousConstSMul : UniformContinuousConstSMul M (α →ᵤ X) where
  uniformContinuous_const_smul c := UniformFun.postcomp_uniformContinuous <| uniformContinuous_const_smul c

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