Prove2Me

Cardinality_of_Empty_Set

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cardinalityempty-setfinite-setsproofwiki

\cardS=0  ⟺  S=\O\card S = 0 \iff S = \O That is, the empty set is finite, and has a cardinality of zero.

Preamble
import Mathlib.Data.Fintype.Card
Formal statement
theorem Cardinality_of_Empty_Set {S : Type _} [Fintype S] : Fintype.card S = 0 ↔ IsEmpty S := by sorry
Source
https://proofwiki.org/wiki/Cardinality_of_Empty_Set

View graph