diff options
Diffstat (limited to 'library/set')
| -rw-r--r-- | library/set/bipartition.tex | 72 | ||||
| -rw-r--r-- | library/set/cantor.tex | 18 | ||||
| -rw-r--r-- | library/set/cons.tex | 112 | ||||
| -rw-r--r-- | library/set/equinumerosity.tex | 68 | ||||
| -rw-r--r-- | library/set/filter.tex | 97 | ||||
| -rw-r--r-- | library/set/fixpoint.tex | 48 | ||||
| -rw-r--r-- | library/set/partition.tex | 50 | ||||
| -rw-r--r-- | library/set/powerset.tex | 107 | ||||
| -rw-r--r-- | library/set/product.tex | 118 | ||||
| -rw-r--r-- | library/set/regularity.tex | 70 | ||||
| -rw-r--r-- | library/set/suc.tex | 70 | ||||
| -rw-r--r-- | library/set/symdiff.tex | 45 |
12 files changed, 875 insertions, 0 deletions
diff --git a/library/set/bipartition.tex b/library/set/bipartition.tex new file mode 100644 index 0000000..e6a76dc --- /dev/null +++ b/library/set/bipartition.tex @@ -0,0 +1,72 @@ +% The theory of splitting sets into two (inhabited, disjoint) partitions. + +% See also "bisections" here: https://isarmathlib.org/Partitions_ZF.html + +\import{set.tex} +\import{set/cons.tex} +\import{set/powerset.tex} + +\subsection{Bipartitions} + +\begin{abbreviation}\label{bipartitions} + $C$ is partitioned by $A$ and $B$ iff $A,B\neq\emptyset$ and $A$ is disjoint from $B$ and $A\union B = C$. +\end{abbreviation} + +\begin{definition}\label{bipartitions_of_a_set} + $\bipartitions{X} = \{ p\in\pow{X}\times\pow{X}\mid \text{$X$ is partitioned by $\fst{p}$ and $\snd{p}$}\}$. +\end{definition} + +\begin{abbreviation}\label{is_a_bipartition_of} + $P$ is a bipartition of $X$ iff $P\in\bipartitions{X}$. +\end{abbreviation} + +\begin{proposition}\label{bipartition_intro} + Suppose $C$ is partitioned by $A$ and $B$. + Then $(A, B)$ is a bipartition of $C$. +\end{proposition} +\begin{proof} + $(A,B)\in\pow{C}\times\pow{C}$. + $C$ is partitioned by $\fst{(A,B)}$ and $\snd{(A,B)}$. + Thus $(A, B)$ is a bipartition of $C$ by \cref{bipartitions_of_a_set}. +\end{proof} + +\begin{proposition}\label{bipartition_elim} + Suppose $(A, B)$ is a bipartition of $C$. + Then $C$ is partitioned by $A$ and $B$. +\end{proposition} +\begin{proof} + $\fst{(A, B)} = A$. + $\snd{(A, B)} = B$. +\end{proof} + +\begin{proposition}\label{bipartitions_emptyset} + $\bipartitions{\emptyset}$ is empty. +\end{proposition} + +\begin{proposition}\label{union_eq_cons_implies_union_remove_eq} + Suppose $d\notin C$. + Suppose $A\union B = \cons{d}{C}$. + Suppose $A, B\neq \{d\}$. + Then $\remove{d}{A}\union \remove{d}{B} = C$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{bipartitions_cons} + Suppose $d\notin C$. + Suppose $\cons{d}{C}$ is partitioned by $A$ and $B$. + Suppose $A, B\neq \{d\}$. + Then $C$ is partitioned by $\remove{d}{A}$ and $\remove{d}{B}$. +\end{proposition} +\begin{proof} + $\remove{d}{A},\remove{d}{B}\neq\emptyset$. + $\remove{d}{A}\union \remove{d}{B} = C$ by \cref{union_eq_cons_implies_union_remove_eq}. +\end{proof} + +% TODO +%\begin{proposition}\label{singleton_bipartition} +% Suppose $b\notin A$. +% Suppose $A$ and $\{b\}$ bipartition $\cons{b}{C}$. +% Then $A = C$. +%\end{proposition} diff --git a/library/set/cantor.tex b/library/set/cantor.tex new file mode 100644 index 0000000..f7c4b2b --- /dev/null +++ b/library/set/cantor.tex @@ -0,0 +1,18 @@ +\import{set/powerset.tex} +\import{function.tex} + +\subsection{Cantor's theorem} + + +\begin{theorem}[Cantor]\label{cantor} + There exists no surjection from $A$ to $\pow{A}$. +\end{theorem} +\begin{proof} + Suppose not. + Consider a surjection $f$ from $A$ to $\pow{A}$. + Let $B = \{a \in A \mid a\notin f(a)\}$. + Then $B\in\pow{A}$. + There exists $a'\in A$ such that $f(a') = B$ by \hyperref[surj]{the definition of surjectivity}. + Now $a' \in B$ iff $a' \notin f(a') = B$. + Contradiction. +\end{proof} 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} diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex new file mode 100644 index 0000000..a846b78 --- /dev/null +++ b/library/set/equinumerosity.tex @@ -0,0 +1,68 @@ +\import{set/powerset.tex} +\import{set/fixpoint.tex} +\import{function.tex} + + +\begin{definition}\label{equinum} + $A$ is equinumerous with $B$ iff there exists a bijection from $A$ to $B$. +\end{definition} + +\begin{abbreviation}\label{approx} + $A\approx B$ iff $A$ is equinumerous with $B$. +\end{abbreviation} + +\begin{proposition}\label{equinum_refl} + $A\approx A$. +\end{proposition} +\begin{proof} + $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}. + Follows by \cref{equinum}. +\end{proof} + +\begin{proposition}\label{equinum_sym} + Suppose $A\approx B$. Then $B\approx A$. +\end{proposition} +\begin{proof} + Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}. + Follows by \cref{equinum}. +\end{proof} + +\begin{proposition}\label{equinum_tran} + Suppose $A\approx B\approx C$. Then $A\approx C$. +\end{proposition} +\begin{proof} + Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Take a bijection $g$ from $B$ to $C$ by \cref{equinum}. + Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}. + Follows by \cref{equinum}. +\end{proof} + + + +\begin{theorem}[Cantor--Schröder--Bernstein]\label{cantorschroederbernstein} + Let $f$ be an injective function from $A$ to $B$. + Let $g$ be an injective function from $B$ to $A$. + Then $A\approx B$. +\end{theorem} +\begin{proof} + Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$. + %By construction: $h$ is a relation. + %By construction: $h$ is right-unique. + %By construction: $\dom{h} = \pow{A}$. + For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}. + Thus $h$ is a function from $\pow{A}$ to $\pow{A}$. + + $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating). + + Take a fixpoint $X$ of $h$ by \cref{knastertarski}. + Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}. + + $\img{g}{B\setminus\img{f}{X}}\subseteq A$. + + Thus $\img{g}{B\setminus\img{f}{X}} = A\setminus X$ by \cref{double_relative_complement}. + + Let $h' = \restrl{h}{X}$. + + Omitted. % TODO +\end{proof} diff --git a/library/set/filter.tex b/library/set/filter.tex new file mode 100644 index 0000000..2797d86 --- /dev/null +++ b/library/set/filter.tex @@ -0,0 +1,97 @@ +\import{set.tex} +\import{set/powerset.tex} + +\section{Filters} + +\begin{abbreviation}\label{upwardclosed} + $F$ is upward-closed in $S$ iff + for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$. +\end{abbreviation} + +\begin{definition}\label{filter} + $F$ is a filter on $S$ iff + $F$ is a family of subsets of $S$ + and $S$ is inhabited + and $S\in F$ + and $\emptyset\notin F$ + and $F$ is closed under binary intersections + and $F$ is upward-closed in $S$. +\end{definition} + +\begin{definition}\label{principalfilter} + $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$. +\end{definition} + +%\begin{proposition}\label{principalfilter_domain_inhabited} +% Suppose $F$ is a filter on $S$. +% Then $S$ is inhabited. +%\end{proposition} + +\begin{proposition}\label{principalfilter_is_filter} + Suppose $A\subseteq S$. + Suppose $A$ is inhabited. + Then $\principalfilter{S}{A}$ is a filter on $S$. +\end{proposition} +\begin{proof} + $S$ is inhabited. % since $A$ is inhabited and $A\subseteq S$. + $\principalfilter{S}{A}$ is a family of subsets of $S$. + $S\in \principalfilter{S}{A}$. + $\emptyset\notin \principalfilter{S}{A}$. + $\principalfilter{S}{A}$ is closed under binary intersections. + $\principalfilter{S}{A}$ is upward-closed in $S$. + Follows by \cref{filter}. +\end{proof} + +\begin{proposition}\label{principalfilter_elem_generator} + Suppose $A\subseteq S$. + $A\in\principalfilter{S}{A}$. +\end{proposition} +\begin{proof} + $A\in\pow{S}$. +\end{proof} + +\begin{proposition}\label{principalfilter_notelem_implies_notsupseteq} + Let $X\in\pow{S}$. + Suppose $X\notin\principalfilter{S}{A}$. + Then $A\not\subseteq X$. +\end{proposition} +\begin{proof} +\end{proof} + +\begin{definition}\label{maximalfilter} + $F$ is a maximal filter on $S$ iff + $F$ is a filter on $S$ and there exists no filter $F'$ on $S$ such that $F\subset F'$. +\end{definition} + +\begin{proposition}\label{principalfilter_singleton_is_filter} + Suppose $a\in S$. + Then $\principalfilter{S}{\{a\}}$ is a filter on $S$. +\end{proposition} +\begin{proof} + $\{a\}\subseteq S$. + $\{a\}$ is inhabited. + Follows by \cref{principalfilter_is_filter}. +\end{proof} + +\begin{proposition}\label{principalfilter_singleton_is_maximal_filter} + Suppose $a\in S$. + Then $\principalfilter{S}{\{a\}}$ is a maximal filter on $S$. +\end{proposition} +\begin{proof} + $\{a\}\subseteq S$. + $\{a\}$ is inhabited. + Thus $\principalfilter{S}{\{a\}}$ is a filter on $S$ by \cref{principalfilter_is_filter}. + It suffices to show that there exists no filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$. + Suppose not. + Take a filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$. + Take $X\in F'$ such that $X\notin \principalfilter{S}{\{a\}}$. + $X\in\pow{S}$. + Thus $\{a\}\not\subseteq X$ by \cref{principalfilter_notelem_implies_notsupseteq}. + Thus $a\notin X$. + $\{a\}\in F'$ + % TODO clean + by \cref{principalfilter,elem_subseteq,union_intro_left,subset,union_absorb_subseteq_left,subseteq_refl,powerset_intro}. + Thus $\emptyset = X\inter \{a\}$. + Hence $\emptyset\in F'$ by \cref{filter}. + Follows by \hyperref[filter]{contradiction to the definition of a filter}. +\end{proof} diff --git a/library/set/fixpoint.tex b/library/set/fixpoint.tex new file mode 100644 index 0000000..700295b --- /dev/null +++ b/library/set/fixpoint.tex @@ -0,0 +1,48 @@ +\import{set/powerset.tex} +\import{function.tex} + +\subsection{Fixpoints} + +% NOTE: we need to explicitly require that a is an element of the domain, +% otherwise the emptyset becomes a fixpoint when it's not in the domain. +\begin{definition}\label{fixpoint} + $a$ is a fixpoint of $f$ iff $a\in\dom{f}$ and $f(a) = a$. +\end{definition} + +\begin{definition}\label{subseteqpreserving} + $f$ is \subseteq-preserving iff + for all $A, B\in\dom{f}$ such that $A\subseteq B$ we have $f(A)\subseteq f(B)$. +\end{definition} + +\begin{theorem}[Knaster--Tarski]\label{knastertarski} + Let $f$ be a \subseteq-preserving function from $\pow{A}$ to $\pow{A}$. + Then there exists a fixpoint of $f$. +\end{theorem} +\begin{proof} + $\dom{f} = \pow{A}$. + Let $P = \{a\in\pow{A}\mid a\subseteq f(a)\}$. + $P\subseteq\pow{A}$. + Thus $\unions{P}\in\pow{A}$. + Hence $f(\unions{P})\in\pow{A}$ by \cref{funs_type_apply}. + + Show $\unions{P}\subseteq f(\unions{P})$. + \begin{subproof} + It suffices to show that every element of $\unions{P}$ is an element of $f(\unions{P})$. + % + Fix $u\in\unions{P}$. + % + Take $p\in P$ such that $u\in p$. + Then $u\in f(p)$. + $p\subseteq\unions{P}$. + $f(p)\subseteq f(\unions{P})$ by \cref{subseteqpreserving}. + Thus $u\in f(\unions{P})$. + \end{subproof} + + Now $f(\unions{P})\subseteq f(f(\unions{P}))$ by \cref{subseteqpreserving}. + Thus $f(\unions{P})\in P$ by definition. + + Hence $f(\unions{P})\subseteq \unions{P}$. + + Thus $f(\unions{P}) = \unions{P}$ by \cref{subseteq_antisymmetric}. + Follows by \cref{fixpoint}. +\end{proof} diff --git a/library/set/partition.tex b/library/set/partition.tex new file mode 100644 index 0000000..ed74bf7 --- /dev/null +++ b/library/set/partition.tex @@ -0,0 +1,50 @@ +\import{set.tex} + +\subsection{Partitions} + +\begin{definition}\label{partition} + $P$ is a partition iff + $\emptyset\notin P$ and + for all $B, C\in P$ such that $B\neq C$ we have $B$ is disjoint from $C$. +\end{definition} + +\begin{abbreviation}\label{partition_of} + $P$ is a partition of $A$ iff + $P$ is a partition and + $\unions{P} = A$. +\end{abbreviation} + +\begin{proposition}\label{partition_emptyset} + $\emptyset$ is a partition of $\emptyset$. +\end{proposition} + +\begin{definition}\label{partition_refinement} + $P'$ is a refinement of $P$ iff + for every $A'\in P'$ there exists + $A\in P$ such that $A'\subseteq A$. +\end{definition} + +\begin{abbreviation}\label{partition_refines} + $P'\refines P$ iff + $P'$ is a refinement of $P$. +\end{abbreviation} + +\begin{proposition}\label{partition_refinement_transitive} + Suppose $P''\refines P'\refines P$. + Then $P''\refines P$. +\end{proposition} +\begin{proof} + It suffices to show that for all $A''\in P''$ there exists $A\in P$ such that $A''\subseteq A$. + Fix $A''\in P''$. + Take $A'\in P'$ such that $A''\subseteq A'$ + by \cref{partition_refinement}. + Take $A\in P$ such that $A'\subseteq A$. + Then $A''\subseteq A$. + Follows by definition. %i.e. A will do for the current existential goal. +\end{proof} + +%\begin{definition}\label{set_of_representatives} +% $X$ is a set of representatives for $P$ iff +% for all $A\in P$ there exists $a\in A$ such that +% $X\inter A = \{a\}$. +%\end{definition} diff --git a/library/set/powerset.tex b/library/set/powerset.tex new file mode 100644 index 0000000..80da4cb --- /dev/null +++ b/library/set/powerset.tex @@ -0,0 +1,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} diff --git a/library/set/product.tex b/library/set/product.tex new file mode 100644 index 0000000..bc7d314 --- /dev/null +++ b/library/set/product.tex @@ -0,0 +1,118 @@ +\import{set.tex} + +\begin{proposition}\label{times_subseteq_left} + Suppose $A\subseteq C$. Then $A\times B\subseteq C\times B$. +\end{proposition} +\begin{proof} + It suffices to show that for all $w\in A\times B$ we have $w\in C\times B$. +\end{proof} + +\begin{proposition}\label{times_subseteq_right} + Suppose $B\subseteq D$. Then $A\times B\subseteq A\times D$. +\end{proposition} +\begin{proof} + It suffices to show that for all $w\in A\times B$ we have $w\in A\times D$. +\end{proof} + +\begin{proposition}\label{inter_times_intro} + Suppose $w\in(A\inter B)\times (C\inter D)$. + Then $w\in(A\times C)\inter (B\times D)$. +\end{proposition} +\begin{proof} + Take $a,c$ such that $w = (a, c)$ + by \cref{times_elem_is_tuple}. + Then $a\in A, B$ and $c\in C,D$ + by \cref{times_tuple_elim,inter}. + Thus $w\in (A\times C), (B\times D)$. +\end{proof} + +\begin{proposition}\label{inter_times_elim} + Suppose $w\in(A\times C)\inter (B\times D)$. + Then $w\in(A\inter B)\times (C\inter D)$. +\end{proposition} +\begin{proof} + $w\in A\times C$. + Take $a, c$ such that $w = (a, c)$. + $a\in A, B$ by \cref{inter,times_tuple_elim}. + $c\in C, D$ by \cref{inter,times_tuple_elim}. + Thus $(a,c) \in (A\inter B)\times (C\inter D)$ by \cref{times,inter_intro}. +\end{proof} + +\begin{proposition}\label{inter_times} + $(A\inter B)\times (C\inter D) = (A\times C)\inter (B\times D)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inter_times_right} + $(X\inter Y)\times Z = (X\times Z)\inter (Y\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inter_times_left} + $X\times (Y\inter Z) = (X\times Y)\inter (X\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_intro} + Suppose $w\in(A\union B)\times (C\union D)$. + Then $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proposition} +\begin{proof} + Take $a,c$ such that $w = (a, c)$. + $a\in A$ or $a\in B$ by \cref{union_iff,times_tuple_elim}. + $c\in C$ or $c\in D$ by \cref{union_iff,times_tuple_elim}. + Thus $(a, c)\in (A\times C)$ or $(a, c)\in (B\times D)$ or $(a, c)\in (A\times D)$ or $(a, c)\in (B\times C)$. + Thus $(a, c)\in (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proof} + +\begin{proposition}\label{union_times_elim} + Suppose $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. + Then $w\in(A\union B)\times (C\union D)$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$w\in(A\times C)$.} + Take $a, c$ such that $w = (a, c) \land a\in A\land c\in C$ by \cref{times}. + Then $a\in A\union B$ and $c\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(B\times D)$.} + Take $b, d$ such that $w = (b, d) \land b\in B\land d\in D$ by \cref{times}. + Then $b\in A\union B$ and $d\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(A\times D)$.} + Take $a, d$ such that $w = (a, d) \land a\in A\land d\in D$ by \cref{times}. + Then $a\in A\union B$ and $d\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(B\times C)$.} + Take $b, c$ such that $w = (b, c) \land b\in B\land c\in C$ by \cref{times}. + Then $b\in A\union B$ and $c\in C\union D$. + Follows by \cref{times_tuple_intro}. + \end{byCase} +\end{proof} + +\begin{proposition}\label{union_times} + $(A\union B)\times (C\union D) = (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_left} + $(X\union Y)\times Z = (X\times Z)\union (Y\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_right} + $X\times (Y\union Z) = (X\times Y)\union (X\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} diff --git a/library/set/regularity.tex b/library/set/regularity.tex new file mode 100644 index 0000000..794d34f --- /dev/null +++ b/library/set/regularity.tex @@ -0,0 +1,70 @@ +\import{set.tex} + +\section{Regularity} + +\begin{abbreviation}\label{elemminimal} + $a$ is an \in-minimal element of $A$ iff + $a\in A$ and $a\notmeets A$. +\end{abbreviation} + +% We need to first state regularity in this slightly weirder form, +% so that we can do \in-induction. +\begin{lemma}% +\label{regularity_aux} + For all $a, A$ such that $a\in A$ + there exists $b\in A$ such that + $b\notmeets A$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $a$] + \begin{byCase} + \caseOf{$a\notmeets b$.} + Straightforward. + \caseOf{$a\meets b$.} + Take $a'$ such that $a'\in a, b$. + Straightforward. % we apply the induction hypothesis to a' + \end{byCase} +\end{proof} + +\begin{proposition}[Regularity]% +\label{regularity} + Let $A$ be an inhabited set. + Then there exists a \in-minimal element of $A$. +\end{proposition} +\begin{proof} + Follows by \cref{regularity_aux,inhabited}. +\end{proof} + + +% Isabelle/ZF-style foundation for case analysis +\begin{theorem}[Foundation]\label{foundation} + Let $A$ be a set. + Then $A = \emptyset$ or there exists $a\in A$ + such that for all $x\in a$ we have $x\notin A$. +\end{theorem} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.} + Straightforward. + \caseOf{$A$ is inhabited.} + Take $a$ such that $a$ is a \in-minimal element of $A$. + Then for all $x\in a$ we have $x\notin A$. + \end{byCase} +\end{proof}. + +\begin{proposition}\label{in_irrefl} + For all sets $A$ we have $A\not\in A$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Straightforward. +\end{proof} + +\begin{proposition}\label{in_implies_neq} + If $a\in A$, then $a\neq A$. +\end{proposition} + +\begin{proposition}\label{in_asymmetric} + For all sets $a, b$ such that $a\in b$ we have $b\notin a$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $a$] + Straightforward. +\end{proof} diff --git a/library/set/suc.tex b/library/set/suc.tex new file mode 100644 index 0000000..3776045 --- /dev/null +++ b/library/set/suc.tex @@ -0,0 +1,70 @@ +\import{set/cons.tex} +\import{set/regularity.tex} + +\subsection{Successor} + +\begin{definition}\label{suc} + $\suc{x} = \cons{x}{x}$. +\end{definition} + +\begin{proposition}\label{suc_intro_self} + $x\in\suc{x}$. +\end{proposition} + +\begin{proposition}\label{suc_intro_in} + Suppose $x\in y$. Then $x\in\suc{y}$. +\end{proposition} + +\begin{proposition}\label{suc_elim} + Suppose $x\in\suc{y}$. + Then $x = y$ or $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_iff} + $x\in\suc{y}$ iff $x = y$ or $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_neq_emptyset} + $\suc{x}\neq \emptyset$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_implies_in} + Suppose $\suc{x}\subseteq y$. Then $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_neq_self} + $\suc{x}\neq x$. +\end{proposition} + +\begin{proposition}\label{suc_injective} + Suppose $\suc{x} = \suc{y}$. Then $x = y$. +\end{proposition} +\begin{proof} + Suppose not. + $\suc{x}\subseteq \suc{y}$. Hence $x\in\suc{y}$. + Then $x\in y$. + $\suc{y}\subseteq \suc{x}$. Hence $y\in\suc{x}$. + Then $y\in x$. + Contradiction. +\end{proof} + +\begin{proposition}\label{subseteq_self_suc_intro} + $x\subseteq\suc{x}$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_intro} + Suppose $x\in y$ and $x\subseteq y$. + Then $\suc{x}\subseteq y$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_elim} + Suppose $\suc{x}\subseteq y$. + Then $x\in y$ and $x\subseteq y$. +\end{proposition} + +\begin{proposition}\label{suc_next_subset} + There exists no $z$ such that $x\subset z\subset \suc{x}$. +\end{proposition} +\begin{proof} + Follows by \cref{suc,subset,subseteq,subset_witness,suc_elim}. +\end{proof} diff --git a/library/set/symdiff.tex b/library/set/symdiff.tex new file mode 100644 index 0000000..61f7448 --- /dev/null +++ b/library/set/symdiff.tex @@ -0,0 +1,45 @@ +\subsection{Symmetric difference} + +\import{set.tex} + +\begin{definition}\label{symdiff} + $x\symdiff y = (x\setminus y)\union (y\setminus x)$. +\end{definition} + +\begin{proposition}% +\label{symdiff_as_setdiff} + $x\symdiff y = (x\union y)\setminus (y\inter x)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{symdiff_implies_xor_in} + If $z\in x\symdiff y$, then either $z\in x$ or $z\in y$. +\end{proposition} + +\begin{proposition}% +\label{xor_in_implies_symdiff} + If either $z\in x$ or $z\in y$, then $z\in x\symdiff y$. +\end{proposition} +\begin{proof} + If $z\in x$ and $z\not\in y$, then $z\in x\setminus y$. + If $z\not\in x$ and $z\in y$, then $z\in y\setminus x$. +\end{proof} + +\begin{proposition}% +\label{symdiff_assoc} + $x\symdiff (y\symdiff z) = (x\symdiff y)\symdiff z$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{symdiff_comm} + $x\symdiff y = y\symdiff x$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} |