two_lt_card_iff — Mathlib

English

For a finite type α, the inequality 2 < |α| is equivalent to the existence of three pairwise distinct elements a, b, c in α.

Русский

Для конечного множества α неравенство 2 < |α| эквивалентно существованию трёх попарно различных элементов a, b, c ∈ α.

LaTeX

$$$2 < |\\alpha| \\iff \\exists a,b,c \\in \\alpha, a \\neq b \\land a \\neq c \\land b \\neq c$$$

Lean4

nonrec theorem two_lt_card_iff : 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c := by
  simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]

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