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