1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
\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{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{cons_subseteq_elim}
Suppose $\cons{x}{Y}\subseteq X$.
Then $x\in X$ and $Y\subseteq X$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{cons_subseteq_iff}
$\cons{x}{Y}\subseteq X$ iff $x\in X$ and $Y\subseteq X$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{subseteq_cons_right}
If $C\subseteq B$, then $C\subseteq \cons{a}{B}$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\begin{corollary}\label{subseteq_cons_self}
$X\subseteq \cons{y}{X}$.
\end{corollary}
\begin{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\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{proof}
Follows by \cref{cons_iff,subseteq}.
\end{proof}
\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{proof}
Follows by \cref{subseteq_cons_intro_right,subseteq_cons_intro_left,subseteq_cons_elim}.
\end{proof}
\begin{proposition}\label{remove_point_eq_setminus_singleton}
$\remove{a}{B} = B\setminus\{a\}$.
\end{proposition}
\begin{proof}
Follows by \cref{setext}.
\end{proof}
\begin{proposition}\label{union_eq_cons}
$\{a\}\union B = \cons{a}{B}$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,setext,union_iff}.
\end{proof}
\begin{proposition}\label{cons_comm}
$\cons{a}{\cons{b}{C}} = \cons{b}{\cons{a}{C}}$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,setext}.
\end{proof}
\begin{proposition}\label{cons_absorb}
Suppose $a\in A$.
Then $\cons{a}{A} = A$.
\end{proposition}
\begin{proof}
Follows by \cref{cons_iff,setext}.
\end{proof}
\begin{proposition}\label{cons_remove}
Suppose $a\in A$.
Then $\cons{a}{A\setminus\{a\}} = A$.
\end{proposition}
\begin{proof}
We have for all $x\in\cons{a}{A\setminus\{a\}}$ we have $x\in A$
by \cref{cons_iff,setminus}.
We have for all $x\in A$ we have $x\in\cons{a}{A\setminus\{a\}}$
by \cref{cons_iff,setminus}.
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 \cref{cons_iff,setext}.
\end{proof}
\begin{proposition}\label{inters_cons}
Suppose $B$ is inhabited.
Then $\inters{\cons{a}{B}} = a\inter\inters{B}$.
\end{proposition}
\begin{proof}
Follows by \cref{inters_iff_forall,cons_iff,inter_intro,inter_elim_left,inter_elim_right,setext}.
\end{proof}
|
