English
Let s be a finite set. Then |s| = 4 iff there exist pairwise distinct x, y, z, w with s = {x, y, z, w}.
Русский
Пусть s — конечное множество. Тогда |s| = 4 эквивалентно существованию четырех попарно различных элементов x, y, z, w с s = {x, y, z, w}.
LaTeX
$$$|s| = 4 \\iff \\exists x \\exists y \\exists z \\exists w\\,\\Bigl(x \\neq y \\land x \\neq z \\land x \\neq y \\land y \\neq z \\land y \\neq w \\land z \\neq w \\Bigr) \\land s = \\{ x, y, z, w \\}$$$
Lean4
theorem card_eq_four : #s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = { x, y, z, w } :=
by
constructor
· rw [card_eq_succ]
grind [card_eq_three]
· grind
