toReal_eq_toReal — Mathlib

English

If x and y are not top or bottom, then x.toReal = y.toReal iff x = y.

Русский

Если x и y не равны верхнему и нижнему пределам, то x.toReal = y.toReal тогда и только тогда, когда x = y.

LaTeX

$$For $x,y \in EReal$ with $x \neq \top$, $x \neq \bot$, $y \neq \top$, $y \neq \bot$, we have $x.toReal = y.toReal \iff x = y$.$$

Lean4

theorem toReal_eq_toReal {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥) (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) :
    x.toReal = y.toReal ↔ x = y := by
  lift x to ℝ using ⟨hx_top, hx_bot⟩
  lift y to ℝ using ⟨hy_top, hy_bot⟩
  simp

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