This commit is contained in:
parent
340e034fdf
commit
430ad82e8b
4 changed files with 14 additions and 11 deletions
|
@ -93,7 +93,7 @@ $\ZFC$ consists of the following axioms:
|
||||||
The axiom of infinity says that there exists and inductive set.
|
The axiom of infinity says that there exists and inductive set.
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
\begin{axiomscheme}[Separation]
|
\begin{axiomschema}[\vocab{Separation}]
|
||||||
% TODO :(Aus)
|
% TODO :(Aus)
|
||||||
Let $\phi$ be some fixed
|
Let $\phi$ be some fixed
|
||||||
fist order formula in $\cL_\in$.
|
fist order formula in $\cL_\in$.
|
||||||
|
@ -110,7 +110,7 @@ $\ZFC$ consists of the following axioms:
|
||||||
\[
|
\[
|
||||||
\forall a.~\exists b.~(b = \{x \in a; \phi(x)\}).
|
\forall a.~\exists b.~(b = \{x \in a; \phi(x)\}).
|
||||||
\]
|
\]
|
||||||
\end{axiomscheme}
|
\end{axiomschema}
|
||||||
|
|
||||||
\begin{notation}
|
\begin{notation}
|
||||||
\todo{$\cap, \setminus, \bigcap$}
|
\todo{$\cap, \setminus, \bigcap$}
|
||||||
|
@ -126,21 +126,22 @@ $\ZFC$ consists of the following axioms:
|
||||||
\item $\forall a.~\exists b.~(b = \bigcap a)$.
|
\item $\forall a.~\exists b.~(b = \bigcap a)$.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{remark}
|
\end{remark}
|
||||||
\begin{axiomscheme}[\vocab{Replacement} (Fraenkel)]
|
\begin{axiomschema}[\vocab{Replacement} (Fraenkel)]
|
||||||
Let $\phi$ be some $\cL_{\in }$ formula.
|
Let $\phi$ be some $\cL_{\in }$ formula.
|
||||||
Then
|
Then
|
||||||
\[
|
\[
|
||||||
\forall v_1 .~\exists b.~\forall y.~(y \in b \iff \exists x .~(x \in a \land \phi(x,y,v_1,v_p))).
|
\forall v_1 .~\exists b.~\forall y.~(y \in b \iff \exists x .~(x \in a \land \phi(x,y,v_1,v_p))).
|
||||||
\]
|
\]
|
||||||
\end{axiomscheme}
|
\end{axiomschema}
|
||||||
|
|
||||||
\begin{axiom}[\vocab{Choice}]
|
\begin{axiom}[\vocab{Choice}]
|
||||||
Every family of non-empty sets has a \vocab{choice set}:
|
Every family of non-empty sets has a \vocab{choice set}:
|
||||||
\todo{TODO}
|
\begin{IEEEeqnarray*}{rCl}
|
||||||
\[
|
\forall x .~&(&\\
|
||||||
\forall x.~(\forall y \in x.~x \neq \emptyset \land
|
&& ((\forall y \in x.~y \neq \emptyset) \land (\forall y \in x .~\forall y' \in x .~(y \neq y' \implies y \cap y' = \emptyset))\\
|
||||||
\forall y \in x \forall y' \in x .(y \neq y' \implies x \cap y' = \emptyset) \implies \exists z .~\forall y \in x .~\exists u.~(z \cap y = \{u\})).
|
&& \implies\exists z.~\forall y \in x.~\exists u.~(z \cap y = \{u\})\\
|
||||||
\]
|
&)&
|
||||||
|
\end{IEEEeqnarray*}
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -283,7 +283,7 @@
|
||||||
\end{claim}
|
\end{claim}
|
||||||
\begin{subproof}
|
\begin{subproof}
|
||||||
Suppose that $\dom(r) \subsetneq a$
|
Suppose that $\dom(r) \subsetneq a$
|
||||||
and $\ran(r) \susbsetneq b$.
|
and $\ran(r) \subsetneq b$.
|
||||||
|
|
||||||
Let $x \coloneqq \min(a \setminus \dom(r))$
|
Let $x \coloneqq \min(a \setminus \dom(r))$
|
||||||
and $y \coloneqq \min(b\setminus \ran(r))$.
|
and $y \coloneqq \min(b\setminus \ran(r))$.
|
||||||
|
|
|
@ -93,6 +93,8 @@
|
||||||
\hypersetup{colorlinks, citecolor=violet, urlcolor=blue!80!black, linkcolor=red!50!black, pdfauthor=\@author, pdftitle=\ifdef{\@course}{\@course}{\@title}}
|
\hypersetup{colorlinks, citecolor=violet, urlcolor=blue!80!black, linkcolor=red!50!black, pdfauthor=\@author, pdftitle=\ifdef{\@course}{\@course}{\@title}}
|
||||||
|
|
||||||
\NewFancyTheorem[thmtools = { style = thmredmargin} , group = { big } ]{warning}
|
\NewFancyTheorem[thmtools = { style = thmredmargin} , group = { big } ]{warning}
|
||||||
|
\NewFancyTheorem[thmtools = { style = thmredmarginandfill} , group = { big } ]{axiom}
|
||||||
|
\NewFancyTheorem[thmtools = { style = thmredmarginandfill, name = Axiom Schema} , group = { big } ]{axiomschema}
|
||||||
|
|
||||||
\DeclareSimpleMathOperator{ran} % TODO: ran vs range
|
\DeclareSimpleMathOperator{ran} % TODO: ran vs range
|
||||||
\DeclareSimpleMathOperator{range} % TODO
|
\DeclareSimpleMathOperator{range} % TODO
|
||||||
|
|
|
@ -27,7 +27,7 @@
|
||||||
\input{inputs/lecture_01}
|
\input{inputs/lecture_01}
|
||||||
\input{inputs/lecture_02}
|
\input{inputs/lecture_02}
|
||||||
\input{inputs/lecture_03}
|
\input{inputs/lecture_03}
|
||||||
% \input{inputs/lecture_04}
|
\input{inputs/lecture_04}
|
||||||
\input{inputs/lecture_05}
|
\input{inputs/lecture_05}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue