isLeast_opNorm — Mathlib

English

The operator norm ‖f‖ is the least bound of the set of all nonnegative scalars M such that ∥f x∥ ≤ M ∥x∥ for all x.

Русский

Операторная норма ‖f‖ является наименьшей границей множества неотрицательных M, удовлетворяющих ∥f x∥ ≤ M ∥x∥ для всех x.

LaTeX

$$$\\|f\\| = \\inf \\{ M \\ge 0 \\mid \\forall x, \\|f x\\| \\le M \\|x\\| \\}$$$

Lean4

theorem isLeast_opNorm [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : IsLeast {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} ‖f‖ :=
  by
  refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow
  simp only [setOf_and, setOf_forall]
  refine isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_ <;> continuity

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