toReal_sub — Mathlib

English

If x ≠ ⊤, x ≠ ⊥, y ≠ ⊤, y ≠ ⊥, then toReal(x − y) = toReal(x) − toReal(y).

Русский

Если x и y не равны ⊤ или ⊥ соответственно, то toReal(x − y) = toReal(x) − toReal(y).

LaTeX

$$$$\text{toReal}(x - y) = \text{toReal}(x) - \text{toReal}(y).$$$$

Lean4

theorem toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
    toReal (x - y) = toReal x - toReal y := by
  lift x to ℝ using ⟨hx, h'x⟩
  lift y to ℝ using ⟨hy, h'y⟩
  rfl

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