toEReal_sub — Mathlib

English

If y ≠ ∞ and y ≤ x, then (x − y).toEReal = x.toEReal − y.toEReal.

Русский

Если y ≠ ∞ и y ≤ x, тогда (x − y).toEReal = x.toEReal − y.toEReal.

LaTeX

$$$\forall x,y : \mathbb{R}_{≥0}^{\infty},\ y \neq \infty \land y \le x \Rightarrow (x - y).to\!\mathrm{EReal} = x.to\!\mathrm{EReal} - y.to\!\mathrm{EReal}$$$

Lean4

theorem _root_.ENNReal.toEReal_sub {x y : ℝ≥0∞} (hy_top : y ≠ ∞) (h_le : y ≤ x) :
    (x - y).toEReal = x.toEReal - y.toEReal :=
  by
  lift y to ℝ≥0 using hy_top
  cases x with
  | top => simp [coe_nnreal_eq_coe_real]
  | coe x => simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

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