sign_apply_eq — Mathlib

English

For any real r, sign r ∈ { -1, 0, 1 }, i.e., sign r = -1 or 0 or 1.

Русский

Для любого r ∈ ℝ верно sign r ∈ { -1, 0, 1 }, то есть sign r = -1 или 0 или 1.

LaTeX

$$$\text{sign}(r) = -1 \;\lor\; \text{sign}(r) = 0 \;\lor\; \text{sign}(r) = 1$$$

Lean4

theorem sign_apply_eq (r : ℝ) : sign r = -1 ∨ sign r = 0 ∨ sign r = 1 :=
  by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · exact Or.inl <| sign_of_neg hn
  · exact Or.inr <| Or.inl <| sign_zero
  · exact Or.inr <| Or.inr <| sign_of_pos hp

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