Cardinal Arithmetic

🅟 Mar 25, 2026

  🅤 Apr 05, 2026

DEF-CDAR-ADD. Addition.

For any cardinals $\kappa$ and $\lambda$,

\[\kappa+\lambda = \lvert(\kappa\times\{0\})\cup(\lambda\times\{1\})\rvert.\]

PROP-CDAR-ADD.

If $X$ and $Y$ are disjoint,

\[\lvert X\rvert+\lvert Y\rvert = \lvert X\cup Y\rvert.\]

DEF-CDAR-MUL. Multiplication.

For any cardinals $\kappa$ and $\lambda$,

\[\kappa\cdot\lambda = \lvert\kappa\times\lambda\rvert.\]

PROP-CDAR-MUL.

For any $X$ and $Y$,

\[\lvert X\rvert\cdot\lvert Y\rvert = \lvert X\times Y\rvert.\]

DEF-CDAR-EXP. Exponentiation.

For any cardinals $\kappa$ and $\lambda$,

\[\kappa^\lambda = \lvert\fun(\lambda,\kappa)\rvert.\]

PROP-CDAR-EXP.

For any $X$ and $Y$,

\[\lvert X\rvert^{\lvert Y\rvert} = \lvert\fun(Y,X)\rvert.\]