instNormedSpace — Mathlib

English

The space of bounded continuous maps α →ᵇ β is a NormedSpace over 𝕜; in particular, ‖c • f‖ ≤ ‖c‖ · ‖f‖ for all c ∈ 𝕜 and f.

Русский

Пространство ограниченных непрерывных отображений α →ᵇ β является нормированным пространством над 𝕜; особенно выполняется неравенство ‖c • f‖ ≤ ‖c‖·‖f‖.

LaTeX

$$$‖c\\cdot f‖ ≤ ‖c‖ \\cdot ‖f‖ \\quad \\text{for all } c \\in 𝕜, f ∈ α \\to^b β$$$

Lean4

instance instNormedSpace [NormedField 𝕜] [NormedSpace 𝕜 β] : NormedSpace 𝕜 (α →ᵇ β) :=
  ⟨fun c f => by
    refine norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) ?_
    exact fun x => norm_smul c (f x) ▸ mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _)⟩

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