uniformContinuousConstSMul — Mathlib

English

If M, α, X form the setting with UniformContinuousConstSMul on X, then UniformFunOn α X 𝔖 inherits UniformContinuousConstSMul M (UniformOnFun α X 𝔖).

Русский

Если существует UniformContinuousConstSMul на X, то UniformFunOn α X 𝔖 наследует UniformContinuousConstSMul на UniformOnFun α X 𝔖.

LaTeX

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

Lean4

instance uniformContinuousConstSMul {𝔖 : Set (Set α)} : UniformContinuousConstSMul M (α →ᵤ[𝔖] X) where
  uniformContinuous_const_smul c := UniformOnFun.postcomp_uniformContinuous <| uniformContinuous_const_smul c

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