diff options
Diffstat (limited to 'library/set/equinumerosity.tex')
| -rw-r--r-- | library/set/equinumerosity.tex | 37 |
1 files changed, 27 insertions, 10 deletions
diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex index a922052..7c12d7a 100644 --- a/library/set/equinumerosity.tex +++ b/library/set/equinumerosity.tex @@ -15,7 +15,7 @@ $A\approx A$. \end{proposition} \begin{proof} - $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}. + $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_elem_bijections}. Follows by \cref{equinum}. \end{proof} @@ -23,7 +23,7 @@ Suppose $A\approx B$. Then $B\approx A$. \end{proposition} \begin{proof} - Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}. Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}. Follows by \cref{equinum}. \end{proof} @@ -32,8 +32,8 @@ Suppose $A\approx B\approx C$. Then $A\approx C$. \end{proposition} \begin{proof} - Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. - Take a bijection $g$ from $B$ to $C$ by \cref{equinum}. + Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}. + Take $g$ such that $g$ is a bijection from $B$ to $C$ by \cref{equinum}. Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}. Follows by \cref{equinum}. \end{proof} @@ -46,16 +46,33 @@ Then $A\approx B$. \end{theorem} \begin{proof} + For all $X\in\pow{A}$ we have + $A\setminus \img{g}{B\setminus\img{f}{X}}\subseteq A$ + by \cref{setminus_subseteq}. + For all $X\in\pow{A}$ we have + $A\setminus \img{g}{B\setminus\img{f}{X}}\in\pow{A}$ + by \cref{powerset_intro}. Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$. - %By construction: $h$ is a relation. - %By construction: $h$ is right-unique. - %By construction: $\dom{h} = \pow{A}$. - For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}. - Thus $h$ is a function from $\pow{A}$ to $\pow{A}$. + For all $X\in\pow{A}$ we have + $(X,A\setminus \img{g}{B\setminus\img{f}{X}})\in h$ by assumption. + $h$ is a relation by \cref{relation}. + $h$ is right-unique by \cref{rightunique,pair_eq_iff}. + Thus $h$ is a function by assumption. + For all $X\in\pow{A}$ we have + $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ + by \cref{function_apply_intro}. + For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by assumption. + For all $X$ we have if $X\in\dom{h}$, then $X\in\pow{A}$ + by \cref{dom_iff,pair_eq_iff}. + For all $X$ we have if $X\in\pow{A}$, then $X\in\dom{h}$ + by \cref{dom_iff}. + Thus $\dom{h} = \pow{A}$ by set extensionality. + $h$ is a function to $\pow{A}$ by assumption. + Thus $h$ is a function from $\pow{A}$ to $\pow{A}$ by \cref{funs_intro}. $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating). - Take a fixpoint $X$ of $h$ by \cref{knastertarski}. + Take $X$ such that $X$ is a fixpoint of $h$ by \cref{knastertarski}. Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}. $\img{g}{B\setminus\img{f}{X}}\subseteq A$. |