English
For real p and q ≥ 0, ENNReal.ofReal(p − q) = ENNReal.ofReal(p) − ENNReal.ofReal(q).
Русский
Для действительных p и q ≥ 0: ENNReal.ofReal(p − q) = ENNReal.ofReal(p) − ENNReal.ofReal(q).
LaTeX
$$$ (p \in \mathbb{R}) \ (q \ge 0) \Rightarrow \operatorname{ofReal}(p - q) = \operatorname{ofReal}(p) - \operatorname{ofReal}(q) $$$
Lean4
theorem ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q :=
by
obtain h | h := le_total p q
· rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]
refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_
rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]
