trichotomy — Mathlib

English

For any natural numbers n, a, b, exactly one of the statements n < a, b ≤ n, or n ∈ Ico(a,b) holds.

Русский

Для любых натуральных чисел n, a, b выполняется одно из: n < a, b ≤ n или n ∈ Ico(a,b).

LaTeX

$$$$ n < a \\lor b \\le n \\lor n \\in Ico(a,b). $$$$

Lean4

/-- For any natural numbers n, a, and b, one of the following holds:
1. n < a
2. n ≥ b
3. n ∈ Ico a b
-/
theorem trichotomy (n a b : ℕ) : n < a ∨ b ≤ n ∨ n ∈ Ico a b :=
  by
  by_cases h₁ : n < a
  · left
    exact h₁
  · right
    by_cases h₂ : n ∈ Ico a b
    · right
      exact h₂
    · left
      simp only [Ico.mem, not_and, not_lt] at *
      exact h₂ h₁

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