toReal_add — Mathlib

English

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

Русский

Если x и y конечны, то toReal(x + y) = toReal(x) + toReal(y).

LaTeX

$$$\\\\forall {x,y} \\\\in \\\\mathrm{EReal}, x \\\\neq \\\\top \\\\land x \\\\neq \\\\bot \\\\land y \\\\neq \\\\top \\\\land y \\\\neq \\\\bot \\\\Rightarrow \\\\operatorname{toReal}(x+y) = \\\\operatorname{toReal}(x) + \\\\operatorname{toReal}(y)$$$

Lean4

theorem toReal_add {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

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