English
A three-case induction: zero, positive, and negative cases suffice to prove a property for all real numbers.
Русский
Трёхслойная индукция: ноль, положительный и отрицательный случаи позволяют доказать свойство для всех действительных.
LaTeX
$$$\text{motive}(0) \land (\forall x\in \mathbb{R}_{\ge 0}, 0 < x \Rightarrow motive(x)) \land (\forall x\in \mathbb{R}_{\ge 0}, 0 < x \Rightarrow motive(x) \Rightarrow motive(-x)) \Rightarrow \forall r \in \mathbb{R}, motive(r).$$$
Lean4
/-- A version of `nnreal_induction_on` which splits into three cases (zero, positive and negative)
instead of two. -/
@[elab_as_elim]
theorem nnreal_induction_on' {motive : ℝ → Prop} (zero : motive 0) (pos : ∀ x : ℝ≥0, 0 < x → motive x)
(neg : ∀ x : ℝ≥0, 0 < x → motive x → motive (-x)) (r : ℝ) : motive r :=
by
obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy
all_goals simp_all
