opNNNorm_le_iff — Mathlib

English

The NNReal-norm of the composition h ∘ f is at most the product of the NNReal-norms: ‖h ∘ f‖₊ ≤ ‖h‖₊ · ‖f‖₊.

Русский

Нормa композиции не больше произведения норм: ‖h ∘ f‖₊ ≤ ‖h‖₊ · ‖f‖₊.

LaTeX

$$$\\|h \\circ f\\|_{+} \\le \\|h\\|_{+} \\cdot \\|f\\|_{+}$$$

Lean4

theorem opNNNorm_le_iff {f : E →SL[σ₁₂] F} {C : ℝ≥0} : ‖f‖₊ ≤ C ↔ ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊ :=
  opNorm_le_iff C.2

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