three_le — Mathlib

English

If 3 ≤ |α|, then for any x,y ∈ α there exists z with z ≠ x and z ≠ y.

Русский

Если 3 ≤ |α|, то для любых x,y ∈ α существует z, отличный от x и от y.

LaTeX

$$$3 \\le |\\alpha| \\Rightarrow \\forall x,y\\in \\alpha, \\exists z\\, (z \\neq x \\land z \\neq y)$$$

Lean4

theorem three_le {α : Type*} (h : 3 ≤ #α) (x : α) (y : α) : ∃ z : α, z ≠ x ∧ z ≠ y :=
  by
  have : ↑(3 : ℕ) ≤ #α := by simpa using h
  have : ↑(2 : ℕ) < #α := by rwa [← succ_le_iff, ← Cardinal.nat_succ]
  have := exists_notMem_of_length_lt [x, y] this
  simpa [not_or] using this

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