toReal_le_toReal — Mathlib

English

If x ≤ y, x ≠ ⊥, and y ≠ ⊤, then x.toReal ≤ y.toReal.

Русский

Если x ≤ y, x ≠ ⊥ и y ≠ ⊤, то x.toReal ≤ y.toReal.

LaTeX

$$$x \le y \land x \neq \bot \land y \neq \top \Rightarrow x^{\mathrm{toReal}} \le y^{\mathrm{toReal}}$$$

Lean4

theorem toReal_le_toReal {x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) : x.toReal ≤ y.toReal :=
  by
  lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
  lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
  simpa using h

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