nnnorm_def — Mathlib

English

The NNReal-norm of the left-multiplication operator by R is equal to 1.

Русский

NNNorm левого умножения на R равен единице: ‖mul 𝕜 R‖₊ = 1.

LaTeX

$$$\\|mul_{\\mathbb{K},R}\\|_{nn} = 1$$$

Lean4

theorem nnnorm_def (f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf {c | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊} :=
  by
  ext
  rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]
  simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk, exists_prop]

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