English
There exist a, b, c, d in s with all pairwise distinct.
Русский
Существуют a, b, c, d в s попарно различны.
LaTeX
$$$|s| > 3 \\iff \\exists a \\in s \\exists b \\in s \\exists c \\in s \\exists d \\in s, a \\neq b \\land a \\neq c \\land a \\neq d \\land b \\neq c \\land b \\neq d \\land c \\neq d$$$
Lean4
theorem three_lt_card_iff :
3 < #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d := by
classical
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four, ← exists_and_left,
exists_comm (α := Finset α)]
constructor
· rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
· rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
exact ⟨a, b, c, d, { a, b, c, d }, by simp_all [insert_subset_iff]⟩
