abs_le_one_iff — Mathlib

English

For any integer a, |a| ≤ 1 iff a ∈ {0,1,-1}.

Русский

Для любого целого a: |a| ≤ 1 эквивалентно a ∈ {0,1,-1}.

LaTeX

$$$ |a| \le 1 \iff a \in \{0,1,-1\}. $$$

Lean4

theorem abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1 :=
  by
  rw [le_iff_lt_or_eq, abs_lt_one_iff]
  match a with
  | (n : ℕ) => simp [abs_eq_natAbs]
  |
  -[n+1] =>
    simp only [negSucc_ne_zero, abs_eq_natAbs, natAbs_negSucc, succ_eq_add_one, Int.natCast_add, cast_ofNat_Int,
      add_eq_right, natCast_eq_zero, false_or, reduceNeg]
    rw [negSucc_eq]
    cutsat

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