enorm'_le_iff_norm_le — Mathlib

English

Inequality of ENNorms is equivalent to inequality of norms.

Русский

Неравенство ENNORM эквивалентно неравенству норм.

LaTeX

$$$\\|x\\|_e \\le \\|y\\|_e \\iff \\|x\\| \\le \\|y\\|$$$

Lean4

@[to_additive enorm_le_iff_norm_le]
theorem enorm'_le_iff_norm_le {x : E} {y : F} : ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖ :=
  by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
  rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h
  exact h

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