instIsBoundedSMul — Mathlib

English

The space α →ᵇ β is a 𝕜–module with IsBoundedSMul, i.e., the scalar action is compatible with the metric structure and the sup-norm bounds behave well under scaling.

Русский

Пространство α →ᵇ β образует модуль над 𝕜 с условием IsBoundedSMul: скалярное умножение совместимо с метрической структурой и пределы по норме сохраняются под масштабированием.

LaTeX

$$$IsBoundedSMul_{\\mathbb{K}}(\\alpha \\to^{\\mathrm{b}} \\beta)$$$

Lean4

instance instIsBoundedSMul : IsBoundedSMul 𝕜 (α →ᵇ β)
    where
  dist_smul_pair' c f₁
    f₂ := by
    rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]
    intro x
    refine (dist_smul_pair c (f₁ x) (f₂ x)).trans ?_
    gcongr
    apply dist_coe_le_dist
  dist_pair_smul' c₁ c₂
    f := by
    rw [dist_le (by positivity)]
    intro x
    refine (dist_pair_smul c₁ c₂ (f x)).trans ?_
    gcongr
    apply dist_coe_le_dist (g := 0)

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