opNNNorm_eq_of_bounds — Mathlib

English

Given two-sided bound conditions, the norm ‖φ‖₊ equals M when φ is bounded by M and any larger bound is at least M.

Русский

При заданных границах норма φ равна M.

LaTeX

$$$\\|\\phi\\|_{+} = M$ under dual bound conditions$$

Lean4

theorem opNNNorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖₊ ≤ M * ‖x‖₊)
    (h_below : ∀ N, (∀ x, ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M :=
  Subtype.ext <| opNorm_eq_of_bounds (zero_le M) h_above <| Subtype.forall'.mpr h_below

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