toReal_add — Mathlib

English

For a,b not equal to ∞, (a + b).toReal = a.toReal + b.toReal.

Русский

Если a ≠ ∞ и b ≠ ∞, то (a + b).toReal = a.toReal + b.toReal.

LaTeX

$$$\\text{If } a \\neq \\infty \\text{ and } b \\neq \\infty:\\; (a + b)^{\\mathrm{toReal}} = a^{\\mathrm{toReal}} + b^{\\mathrm{toReal}}$$$

Lean4

theorem toReal_add (ha : a ≠ ∞) (hb : b ≠ ∞) : (a + b).toReal = a.toReal + b.toReal :=
  by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  rfl

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