nnnorm_eq_iSup_nnnorm — Mathlib

English

If K ≤ L are compact subsets (in the compacts lattice), then the norm of the restriction is monotone: ‖f.restrict K‖ ≤ ‖f.restrict L‖.

Русский

Если K ≤ L - компакты, то норма ограничения монотонична: ‖f.restrict K‖ ≤ ‖f.restrict L‖.

LaTeX

$$$\|f\restriction K\| \le \|f\restriction L\|$$$

Lean4

theorem nnnorm_eq_iSup_nnnorm : ‖f‖₊ = ⨆ x : α, ‖f x‖₊ :=
  (mkOfCompact f).nnnorm_eq_iSup_nnnorm

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