nnreal_dichotomy — Mathlib

English

For every real r, either r = 0 or there exists x ≥ 0 such that r = x or r = -x.

Русский

Для каждого r ∈ ℝ либо r = 0, либо существует x ≥ 0 такое что r = x или r = -x.

LaTeX

$$$ r = 0 \lor \exists x \in \mathbb{R}_{\ge 0},\; r = x \lor r = -x, $$$

Lean4

/-- Every real number nonnegative or nonpositive, phrased using `ℝ≥0`. -/
theorem nnreal_dichotomy (r : ℝ) : ∃ x : ℝ≥0, r = x ∨ r = -x :=
  by
  obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
  all_goals
    rw [← neg_neg r]
    lift (_ : ℝ) to ℝ≥0 using hr with r
    aesop

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