enorm'_eq_iff_norm_eq — Mathlib

English

Equivalence between equality of ENNorms and equality of norms.

Русский

Эквивалентность между равенством ENNORM и равенством норм.

LaTeX

$$$\\|x\\|_e = \\|y\\|_e \\iff \\|x\\| = \\|y\\|$$$

Lean4

@[to_additive enorm_eq_iff_norm_eq]
theorem enorm'_eq_iff_norm_eq {x : E} {y : F} : ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖ :=
  by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by congr⟩
  exact (Real.toNNReal_eq_toNNReal_iff (norm_nonneg' _) (norm_nonneg' _)).mp (ENNReal.coe_inj.mp h)

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