toNNReal_le_toNNReal — Mathlib

English

If a,b ∈ ENNReal are finite, then a.toNNReal ≤ b.toNNReal iff a ≤ b.

Русский

Если a,b ∈ ENNReal конечны, то a.toNNReal ≤ b.toNNReal эквивалентно a ≤ b.

LaTeX

$$$$ \\forall a,b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq \\infty \\land b \\neq \\infty \\Rightarrow a^{\\mathrm{toNNReal}} \\le b^{\\mathrm{toNNReal}} \\iff a \\le b. $$$$

Lean4

@[simp]
theorem toNNReal_le_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal ≤ b.toNNReal ↔ a ≤ b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe], toNNReal_mono hb⟩

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