1 files changed, 112 insertions, 0 deletions
diff --git a/library/set/cons.tex b/library/set/cons.tex
new file mode 100644
index 0000000..e03ba4f
--- /dev/null
+++ b/library/set/cons.tex
@@ -0,0 +1,112 @@
+\import{set.tex}
+
+\subsection{Additional results about cons}
+
+\begin{proposition}\label{cons_subseteq_intro}
+    Suppose $x\in X$.
+    Suppose $Y\subseteq X$.
+    Then $\cons{x}{Y}\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{cons_subseteq_elim}
+    Suppose $\cons{x}{Y}\subseteq X$.
+    Then $x\in X$ and $Y\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{cons_subseteq_iff}
+    $\cons{x}{Y}\subseteq X$ iff $x\in X$ and $Y\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_cons_right}
+    If $C\subseteq B$, then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+
+\begin{corollary}\label{subseteq_cons_self}
+    $X\subseteq \cons{y}{X}$.
+\end{corollary}
+
+\begin{abbreviation}\label{remove_point}
+    $\remove{a}{B} = B\setminus\{a\}$.
+\end{abbreviation}
+
+\begin{proposition}\label{subseteq_cons_intro_left}
+    Suppose $a\in C \land \remove{a}{C} \subseteq B$.
+    Then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_cons,setminus_eq_emptyset_iff_subseteq}.
+\end{proof}
+
+\begin{proposition}\label{subseteq_cons_intro_right}
+    Suppose $C \subseteq B$.
+    Then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_cons_elim}
+    Suppose $C\subseteq \cons{a}{B}$.
+    Then $C\subseteq B \lor (a\in C \land \remove{a}{C} \subseteq B)$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_cons,subseteq,cons_iff,setminus_eq_emptyset_iff_subseteq}.
+\end{proof}
+
+\begin{proposition}\label{subseteq_cons_iff}
+    $C\subseteq \cons{a}{B}$ iff $C\subseteq B \lor (a\in C \land \remove{a}{C}\subseteq B)$.
+\end{proposition}
+
+
+\begin{proposition}\label{remove_point_eq_setminus_singleton}
+    $\remove{a}{B} = B\setminus\{a\}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+
+\begin{proposition}\label{union_eq_cons}
+    $\{a\}\union B = \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_comm}
+    $\cons{a}{\cons{b}{C}} = \cons{b}{\cons{a}{C}}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_absorb}
+    Suppose $a\in A$.
+    Then $\cons{a}{A} = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_remove}
+    Suppose $a\in A$.
+    Then $\cons{a}{A\setminus\{a\}} = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_idempotent}
+    Then $\cons{a}{\cons{a}{B}} = \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inters_cons}
+    Suppose $B$ is inhabited.
+    Then $\inters{\cons{a}{B}} = a\inter\inters{B}$.
+\end{proposition}
+\begin{proof}
+    $\cons{a}{B}$ is inhabited.
+    Thus for all $c$ we have $c\in\inters{\cons{a}{B}}$ iff $c\in a\inter \inters{B}$
+        by \cref{inters_iff_forall,cons_iff,inter}.
+    Follows by \hyperref[setext]{extensionality}.
+\end{proof}