norm_zero — Mathlib

English

The norm of the zero element is zero: ‖0‖ = 0.

Русский

Норма нулевого элемента равна нулю: ‖0‖ = 0.

LaTeX

$$$$ \|0\| = 0. $$$$

Lean4

@[simp]
theorem norm_zero : ‖(0 : lp E p)‖ = 0 :=
  by
  rcases p.trichotomy with (rfl | rfl | hp)
  · simp [lp.norm_eq_card_dsupport]
  · simp [lp.norm_eq_ciSup]
  · rw [lp.norm_eq_tsum_rpow hp]
    have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'
    simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'

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