blob: 068d6a86068300592adc40eeb9c9e702168445f3 (
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
|
\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}.
\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$.}
Follows by assumption.
\caseOf{$A \neq\emptyset$.}
Take $a$ such that $a$ is a \in-minimal element of $A$ by \cref{nonempty_inhabited,regularity}.
Then for all $x\in a$ we have $x\notin A$.
Follows by assumption.
\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}
|
