two_lt_card — Mathlib

English

There exist a, b, c in s with a, b, c pairwise distinct (membership form).

Русский

Существуют a, b, c в s такие, что они попарно различны (через членство).

LaTeX

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

Lean4

theorem two_lt_card : 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c := by
  simp_rw [two_lt_card_iff, exists_and_left]

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