blob: e03ba4f9f79a94362b1979062d918ccbf3d95798 (
plain)
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
|
\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}
|
