English
Let motive be a target type; there is an induction principle recENNReal splitting EReal into the nonnegative part (viewed via ENNReal) and the negative part (viewed via negation).
Русский
Пусть motive – целевая область; существует принцип индукции recENNReal, разделяющий EReal на неположительную(неотрицательную) часть через ENNReal и отрицательную через отрицание.
LaTeX
$$$$\mathrm{recENNReal}(motive, coe, neg\_coe, x) = \begin{cases} coe\left(x^{\mathrm{toENNReal}}\right), & x \ge 0 \\ neg\_coe(-x), & x < 0 \end{cases}.$$$$
Lean4
/-- Induction principle for `EReal`s splitting into cases `↑(x : ℝ≥0∞)` and `-↑(x : ℝ≥0∞)`.
In the latter case, we additionally assume `0 < x`. -/
@[elab_as_elim]
def recENNReal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x) (neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x))
(x : EReal) : motive x :=
if hx : 0 ≤ x then coe_toENNReal hx ▸ coe _
else
haveI H₁ : 0 < -x := by simpa using hx
haveI H₂ : x = -(-x).toENNReal := by rw [coe_toENNReal H₁.le, neg_neg]
H₂ ▸ neg_coe _ <| by positivity
