mkContinuous_norm_le' — Mathlib

English

The operator norm is compatible with restriction of scalars in a bilinear context, yielding the same bound when passing to a reduced scalar field.

Русский

Норма оператора совместима с ограничением скаляров в билинейном контексте, сохраняя ту же границу при переходе к меньшему полю скаляров.

LaTeX

$$$ \|f \circ g\| \le \|f\| \cdot \|g\| $$$

Lean4

/-- If a continuous linear map is constructed from a linear map via the constructor `mkContinuous`,
then its norm is bounded by the bound or zero if bound is negative. -/
theorem mkContinuous_norm_le' (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : ‖f.mkContinuous C h‖ ≤ max C 0 :=
  ContinuousLinearMap.opNorm_le_bound _ (le_max_right _ _) fun x => (h x).trans <| by gcongr; apply le_max_left

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