English
Let α be a finite type. Then card α ≤ 1 if and only if any two elements of α are equal.
Русский
Пусть α — конечный тип. Тогда card α ≤ 1 тогда и только тогда, когда любые два элемента α равны между собой.
LaTeX
$$$\\operatorname{card} \\alpha \\le 1 \\iff \\forall a,b: \\alpha, a = b$$$
Lean4
theorem card_le_one_iff : card α ≤ 1 ↔ ∀ a b : α, a = b :=
let n := card α
have hn : n = card α := rfl
match n, hn with
| 0, ha => ⟨fun _h => fun a => (card_eq_zero_iff.1 ha.symm).elim a, fun _ => ha ▸ Nat.le_succ _⟩
| 1, ha =>
⟨fun _h => fun a b => by
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
rw [hx a, hx b], fun _ => ha ▸ le_rfl⟩
| n + 2, ha =>
⟨fun h =>
False.elim <| by rw [← ha] at h;
cases h with
| step h => cases h; ,
fun h => card_unit ▸ card_le_of_injective (fun _ => ()) fun _ _ _ => h _ _⟩
