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).

import proveit
%theory

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

All axioms contained within this theory

proveit.logic.sets.cardinality.empty_card

proveit.logic.sets.cardinality.card_induction