nnnorm_eq_iSup_nnnorm — Mathlib

English

The NN-norm of a bounded continuous map equals the iSup of the pointwise NN-norms.

Русский

NN-норма ограниченной непрерывной карты равна iSup точечных NN-норм.

LaTeX

$$$‖f‖_+ = \\big\\lceil\\!\\!\\!⨆ x : α, ‖f x‖_+\\!\\!\\!\\big\\rceil$$$

Lean4

theorem nnnorm_eq_iSup_nnnorm : ‖f‖₊ = ⨆ x : α, ‖f x‖₊ :=
  Subtype.ext <| (norm_eq_iSup_norm f).trans <| by simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]

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