English
A set has cardinality 2 if and only if there exist two distinct elements whose set {x,y} equals the whole universe.
Русский
У множества кардинал равен 2 тогда, когда существуют два различных элемента x,y такие, что множество {x,y} равно всему множеству.
LaTeX
$$$#\\alpha = 2 \\iff \\exists x,y : \\alpha, x \\neq y \\land \\{x,y\\} = \\mathrm{univ}$$$
Lean4
theorem mk_eq_two_iff : #α = 2 ↔ ∃ x y : α, x ≠ y ∧ ({ x, y } : Set α) = univ := by
classical
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
constructor
· rintro ⟨t, ht, x, y, hne, rfl⟩
exact ⟨x, y, hne, by simpa using ht⟩
· rintro ⟨x, y, hne, h⟩
exact ⟨{ x, y }, by simpa using h, x, y, hne, rfl⟩
