logo

Context: proveit.logic.set_theory.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.numbers.sets).

In [1]:
import proveit
%context