contents/computer_science.tex : Better definitions and description && Added AOC implies LEM proof

contents/set_theory.tex

@@ -25,11 +25,34 @@ Il existe un ensemble vide notée $\emptyset$.
 \langsubsection{Paire}{Pairing}
 %TODO Complete subsection
 
+Source: \citeannexes{wikipedia_ordered_pair}
+
+\langsubsubsection{Définition de Wiener}{Wiener's definition}
+
+$(a,b) := \{\{\{a\}, \emptyset\}, \{b\}\}$
+
+\langsubsubsection{Définition de Hausdorff}{Hausdorff's definition}
+
+$(a,b) := \{\{a, 1\}, \{b,2\}\}$ where $a \ne 1 \land b \ne 2$
+
+\langsubsubsection{Définition de Kuratowski}{Kuratowski's definition}
+
+\begin{definition_sq} \label{definition:ordered_pair}
+$(a,b)_K := \{\{a\}, \{a,b\}\}$
+\end{definition_sq}
+
 \langsubsection{Réunion}{Union}
-%TODO Complete section
 
 Unite all elements of two given sets into one.
 
+\begin{definition_sq} \label{definition:set_union}
+$A \union B := \{x | (x \in A \lor x \in B)\}$
+\end{definition_sq}
+
+Pour des ensembles finis : $\forall E,F \in \Cat(\Set), \card{E \union F} = \card{E} + \card{F} - \card{E \intersection F}$
+
+Example :
+
 $n,m \in \N$
 
 $A := \{a_0, \cdots, a_n\}$
@@ -52,28 +75,81 @@ For a set $S$ such that $\card{S} = n \implies \card{\mathbf{P}(S)} = 2^n$
 \langsubsection{Choix}{Choice}
 %TODO Complete subsection
 
+\begin{definition_sq} \label{definition:set_axiom_of_choice}
+For any set $X$ of nonempty sets, there exists a choice function $f$ that is defined on $X$ and maps each set of $X$ to an element of that set i.e.
+
+$$\forall X [\emptyset \notin X \implies \exists \function{f}{X}{\Union_{A \in X} A \quad \forall A \in X(f(A) \in A)}]$$
+\end{definition_sq}
+
+\begin{theorem_sq} \label{theorem:ac_implies_lem}
+The axiom of choice implies the law of excluding middle.
+\end{theorem_sq}
+
+\begin{proof}
+
+Assume that $0 \ne 1$ (or any two elements that are not equal), Let $\Omega := \{0, 1\}$, $p \in \mathbf{Prop}$
+
+$A := \{ x \in \Omega | x = 0 \lor p \}$
+
+$B := \{ y \in \Omega | y = 1 \lor p \}$
+
+$\implies 0 \in A \land 1 \in B$
+
+$X := \{ A, B \}$, by definition $\Union X = \Omega$
+
+By the axiom of choice $\implies \exists \function{f}{X}{\Omega}$
+
+Using this function there are 4 cases:
+\begin{enumerate}[(1)]
+	\item $f(A) = f(B) = 0 \implies 0 \in B$ but $((0 = 1) \lor p \implies \top) \implies p$
+	\item $f(A) = f(B) = 1$ Same reasoning as (1) $\implies p$ % TODO Replace with local labeling and reference
+	\item $f(A) \neq f(B) = 0 \implies A \neq B$ but $p \implies A = B = \Omega$ (contrapositive of (1) and (2)) $\implies \lnot p$
+	\item $f(A) \neq f(B) = 1$ Same reasoning as (3) $\implies \lnot p$
+\end{enumerate}
+
+So by proof by cases $(p \lor \lnot p)$ which is the law of excluded middle \ref{definition:law_excluding_middle}.
+\end{proof}
+
 \section{Intersection}
 
 Unite all common elements of two given sets into one.
 
-$n,m,i \in \N$
+\begin{definition_sq} \label{definition:set_intersection}
+$A \intersection B := \{x | (x \in A \land x \in B)\}$
+\end{definition_sq}
 
-$A = \{a_0, \cdots, a_n, c_0, \cdots, c_n\}$
+Pour des ensembles finis : $\forall E,F \in \Cat(\Set), \card{E \intersection F} = \card{E} - \card{F} + \card{E \union F}$
 
-$B = \{b_0, \cdots, b_m, c_0, \cdots, c_n\}$
+Example :
 
-$A \cap B = \{c_0, \cdots, c_n\}$
+$n,m \in \N$
+
+$A := \{a_0, \cdots, a_n, c_0, \cdots, c_n\}$
+
+$B := \{b_0, \cdots, b_m, c_0, \cdots, c_n\}$
+
+$A \intersection B = \{c_0, \cdots, c_n\}$
 
 \langsection{Différence des sets}{Set difference}
 %TODO Complete section
 
+Exclude elements of a set from a set
+
+\begin{definition_sq} \label{definition:set_difference}
+$A \setminus B := \{x | (x \in A \land x \notin B)\}$
+\end{definition_sq}
+
+Pour des ensembles finis : $\forall E,F \in \Cat(\Set), \card{E \setminus F} = \card{E} - \card{E \intersection F}$
+
 \langsection{Fonction}{Function}
 
 Source: \citeannexes{wikipedia_function_mathematics}
 
+\begin{definition_sq} \label{definition:set_function}
 Une fonction $f$ est un tuple d'un domaine \citeannexes{wikipedia_domain_function} $A$ et un codomaine \citeannexes{wikipedia_codomain} $B$.
+\end{definition_sq}
 
-If the domain is the same as the codomain then the function is an endormorphsim \ref{definition:endomorphism} applied on set theory \ref{set_theory}.
+If the domain is the same as the codomain then the function is an endormorphsim \ref{definition:endomorphism} applied the category \ref{definition:category} of sets \ref{set_theory}.
 
 \subsection{Notation}
 
@@ -81,22 +157,28 @@ $\functiondef{A}{B}$
 
 $\function{f}{x}{f(x)}$
 
-\langsubsection{Injectivité}{Injectivity} \label{definition:injective}
+\langsubsection{Injectivité}{Injectivity}
 
 Source: \citeannexes{wikipedia_injective_function}
 
+\begin{definition_sq} \label{definition:injective}
 Une fonction $f$ de $E$ dans $F$ est dite \textbf{injective} si, et seulement si, $\forall (a,b) \in E, f(a) = f(b) \Rightarrow a = b$.
+\end{definition_sq}
 
-\langsubsection{Surjectivité}{Surjectivity} \label{definition:surjective}
+\langsubsection{Surjectivité}{Surjectivity}
 
 Source: \citeannexes{wikipedia_surjective_function}
 
+\begin{definition_sq} \label{definition:surjective}
 Une fonction $f$ de $E$ dans $F$ est dite \textbf{surjective} si, et seulement si, $\forall y \in F, \exists x \in E : y = f(x)$.
+\end{definition_sq}
 
 \langsubsection{Bijectivité}{Bijectivity}
 
-Source: \citeannexes{wikipedia_bijection} \label{definition:bijection}
+Source: \citeannexes{wikipedia_bijection}
 
+\begin{definition_sq} \label{definition:bijection}
 Une fonction $f$ de $E$ dans $F$ est dite \textbf{bijective} si, et seulement si, elle est à la fois injective \ref{definition:injective} et surjective \ref{definition:surjective} ou $\forall y \in F, \exists! x \in E : y = f(x)$.
+\end{definition_sq}
 
-Every bijection is an isomorphism \ref{definition:isomorphism} applied on set theory \ref{set_theory}.
+Every bijection is an isomorphism \ref{definition:isomorphism} applied on the category \ref{definition:category} of sets \ref{set_theory}.