English
If a property holds for all x ≥ 0 and is preserved under negation, then it holds for all real numbers.
Русский
Если свойство верно для всех x ≥ 0 и сохраняется при заменe x на −x, то оно верно и для всех действительных.
LaTeX
$$$(\forall x \in \mathbb{R}_{\ge 0}, \text{motive}(x)) \wedge (\forall x \in \mathbb{R}_{\ge 0}, \text{motive}(x) \Rightarrow \text{motive}(-x)) \Rightarrow \forall r \in \mathbb{R}, \text{motive}(r).$$$
Lean4
/-- To prove a property holds for real numbers it suffices to show that it holds for `x : ℝ≥0`,
and if it holds for `x : ℝ≥0`, then it does also for `(-↑x : ℝ)`. -/
@[elab_as_elim]
theorem nnreal_induction_on {motive : ℝ → Prop} (nonneg : ∀ x : ℝ≥0, motive x)
(nonpos : ∀ x : ℝ≥0, motive x → motive (-x)) (r : ℝ) : motive r :=
by
obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy
all_goals simp_all
