diff options
Diffstat (limited to 'library/set.tex')
| -rw-r--r-- | library/set.tex | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/library/set.tex b/library/set.tex index 2df4768..d0cbb97 100644 --- a/library/set.tex +++ b/library/set.tex @@ -898,13 +898,25 @@ The $\operatorname{\textsf{cons}}$ operation is set adjunction. $A\setminus \cons{a}{B} = (A\setminus \{a\})\setminus B$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in A\setminus \cons{a}{B}$ we have + $x\in (A\setminus \{a\})\setminus B$ + by \cref{cons_iff,setminus}. + We have for all $x\in (A\setminus \{a\})\setminus B$ we have + $x\in A\setminus \cons{a}{B}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{setminus_cons_flip} $A\setminus \cons{a}{B} = (A\setminus B)\setminus \{a\}$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in A\setminus \cons{a}{B}$ we have + $x\in (A\setminus B)\setminus \{a\}$ + by \cref{cons_iff,setminus}. + We have for all $x\in (A\setminus B)\setminus \{a\}$ we have + $x\in A\setminus \cons{a}{B}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{setminus_disjoint} |