mkContinuous_norm_le — Mathlib

English

The fundamental property of the operator norm in extended norms says that for every x, the extended norm of f x is bounded by the product of extended norms of f and x.

Русский

Фундаментальное свойство операторной нормы в расширенных нормированных пространствах: для каждого x выполняется неравенство нормы f x ≤ (норма f)·(норма x).

LaTeX

$$$ \|f x\|_e \le \|f\|_e \cdot \|x\|_e $$$

Lean4

/-- If a continuous linear map is constructed from a linear map via the constructor `mkContinuous`,
then its norm is bounded by the bound given to the constructor if it is nonnegative. -/
theorem mkContinuous_norm_le (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    ‖f.mkContinuous C h‖ ≤ C :=
  ContinuousLinearMap.opNorm_le_bound _ hC h

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