ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1846 on D15: Set cardinality
Cardinality of set complement
Formulation 0
Let $X$ be a D11: Set such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) $E$ is a D17: Finite set
Then \begin{equation} |X \setminus E| = |X| - |E| \end{equation}
Formulation 1
Let $X$ be a D11: Set such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) \begin{equation} |E| < \infty \end{equation}
Then \begin{equation} |X \setminus E| = |X| - |E| \end{equation}
Subresults
R4189
Proofs
Proof 0
Let $X$ be a D11: Set such that
(i) $E \subseteq X$ is a D78: Subset of $X$
(ii) $E$ is a D17: Finite set
Result R977: Ambient set is union of subset and complement of subset provides the partition $X = E \cup (X \setminus E)$. Result R4321: Set and set complement are disjoint shows that $E$ and its complement $X \setminus E$ are disjoint, so R4322: Cardinality of finite set union of disjoint sets states \begin{equation} |X| = |E \cup (X \setminus E)| = |E| + |X \setminus E| \end{equation} Subtracting the finite quantity $|E|$ from both sides, we have \begin{equation} |X| - |E| = |E| + |X \setminus E| - |E| = |X \setminus E| \end{equation} which is what was required to be shown. $\square$