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
|
\import{set.tex}
\subsection{Powerset}
\begin{abbreviation}\label{powerset_of}
The powerset of $X$ denotes $\pow{X}$.
\end{abbreviation}
\begin{axiom}%
\label{pow_iff}
$B\in\pow{A}$ iff $B\subseteq A$.
\end{axiom}
\begin{proposition}\label{powerset_intro}
Suppose $A\subseteq B$.
Then $A\in\pow{B}$.
\end{proposition}
\begin{proposition}\label{powerset_elim}
Let $A\in\pow{B}$.
Then $A\subseteq B$.
\end{proposition}
\begin{proposition}\label{powerset_bottom}
$\emptyset\in\pow{A}$.
\end{proposition}
\begin{proposition}\label{powerset_top}
$A\in\pow{A}$.
\end{proposition}
\begin{proposition}\label{unions_subseteq_of_powerset_is_subseteq}
Let $A$ be a set.
Let $B$ be a subset of $\pow{A}$.
Then $\unions{B}\subseteq A$.
\end{proposition}
\begin{proof}
Follows by \cref{subseteq,powerset_elim,unions_iff}.
\end{proof}
\begin{corollary}\label{powerset_closed_unions}
Let $A$ be a set.
Let $B$ be a subset of $\pow{A}$.
Then $\unions{B}\in\pow{A}$.
\end{corollary}
\begin{proof}
Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}.
\end{proof}
\begin{proposition}\label{unions_powerset}
$\unions{\pow{A}} = A$.
\end{proposition}
\begin{proof}
Follows by set extensionality.
\end{proof}
\begin{proposition}\label{inters_powerset}
$\inters{\pow{A}} = \emptyset$.
\end{proposition}
\begin{proof}
Follows by set extensionality.
\end{proof}
\begin{proposition}\label{union_powersets_subseteq}
$\pow{A}\union\pow{B} \subseteq \pow{A\union B}$.
\end{proposition}
\begin{proof}
$\pow{A}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_left}.
$\pow{B}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_right}.
Follows by \cref{subseteq,pow_iff,powerset_elim,union_iff,subset_transitive}.
\end{proof}
\begin{proposition}\label{powerset_emptyset}
$\pow{\emptyset} = \{\emptyset\}$.
\end{proposition}
% LATER
%\begin{proposition}\label{powerset_cons}
% Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
%\end{proposition}
\begin{proposition}\label{powerset_union_subseteq}
$\pow{A}\union\pow{B}\subseteq \pow{A\union B}$.
\end{proposition}
\begin{proposition}\label{subseteq_pow_unions}
$A\subseteq\pow{\unions{A}}$.
\end{proposition}
\begin{proof}
Follows by \cref{subseteq,pow_iff,unions_intro}.
\end{proof}
\begin{proposition}\label{unions_pow}
$\unions{\pow{A}} = A$.
\end{proposition}
\begin{proposition}\label{unions_elem_pow_iff}
$\unions{A}\in\pow{B}$ iff $A\in\pow{\pow{B}}$.
\end{proposition}
\begin{proposition}\label{pow_inter}
$\pow{A\inter B} = \pow{A}\inter\pow{B}$.
\end{proposition}
\begin{proof}
Follows by \cref{setext,inter,pow_iff,subseteq_inter_iff}.
\end{proof}
|
