uniformContinuousConstSMul — Mathlib

English

If f is IsUniformInducing and preserves scalar action compatibly, then the induced uniform-continuous scalar multiplication on X is indeed UniformContinuousConstSMul.

Русский

Если f является IsUniformInducing и сохраняет совместность действия скаляров, тогда получшееся равномерно непрерывное умножение — UniformContinuousConstSMul на X.

LaTeX

$$$IsUniformInducing f \rightarrow (\forall c, x, f(c \cdot x) = c \cdot f(x)) \rightarrow UniformContinuousConstSMul M X$$$

Lean4

@[to_additive]
theorem uniformContinuousConstSMul [SMul M Y] [UniformContinuousConstSMul M Y] {f : X → Y} (hf : IsUniformInducing f)
    (hsmul : ∀ (c : M) x, f (c • x) = c • f x) : UniformContinuousConstSMul M X where
  uniformContinuous_const_smul
    c := by simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul] using hf.uniformContinuous.const_smul c

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