ofReal_lt_ofReal_iff — Mathlib

English

Let p,q ∈ ℝ with 0 < q. Then ENNReal.ofReal p < ENNReal.ofReal q if and only if p < q.

Русский

Пусть p,q ∈ ℝ и 0 < q. Тогда ENNReal.ofReal p < ENNReal.ofReal q тогда и только если p < q.

LaTeX

$$$ (0 < q) \Rightarrow ENNReal.ofReal(p) < ENNReal.ofReal(q) \iff p < q $$$

Lean4

@[simp]
theorem ofReal_lt_ofReal_iff {p q : ℝ} (h : 0 < q) : ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]

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