English
For any α, the natural-cardinality Nat.card α equals the finite-cardinality Fintype.card α if α is finite, and equals 0 otherwise.
Русский
Для любого α натуральная кардинал Nat.card α равна конечной кардинальности Fintype.card α, если α конечен, и равна 0 в противном случае.
LaTeX
$$$Nat.card(\alpha) = if\ Finite(\alpha) then Fintype.card(\alpha) else 0$$$
Lean4
theorem card_eq (α : Type*) : Nat.card α = if _ : Finite α then @Fintype.card α (Fintype.ofFinite α) else 0 :=
by
cases finite_or_infinite α
· letI := Fintype.ofFinite α
simp only [this, *, Nat.card_eq_fintype_card, dif_pos]
· simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]
