Theory of proveit.logic.sets.cardinality

The cardinality of set $S$, $|S|$, is the number of unique elements of $S$ if $S$ is a finite set. The cardinality of infinite sets are specially defined quantities such as $\aleph_0$ that are appropriately defined where these infinite sets are defined (see proveit.numberss.sets).

In [1]:
import proveit

Local content of this theory

All axioms contained within this theory