coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal

English

For any real x, x in EReal equals toNNReal(x) minus toNNReal(-x).

Русский

Для любого вещественного x соответствие x в EReal равно toNNReal(x) минус toNNReal(-x).

LaTeX

$$$$x \in \mathbb{R} \Rightarrow x^{\mathrm{EReal}} = \mathrm{toNNReal}(x) - \mathrm{toNNReal}(-x).$$$$

Lean4

theorem coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (x : ℝ) : (x : EReal) = Real.toNNReal x - Real.toNNReal (-x) :=
  by
  rcases le_total 0 x with (h | h)
  · lift x to ℝ≥0 using h
    rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero, coe_ennreal_zero,
      sub_zero]
    rfl
  · rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real, Real.coe_toNNReal,
      zero_sub, coe_neg, neg_neg]
    exact neg_nonneg.2 h

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