\langchapter{Théorie des ensembles}{Set theory} \label{set_theory}
%TODO Complete chapter

Source: \citeannexes{wikipedia_set_theory}

Un ensemble est une construction mathématique qui réuni plusieurs objets en une même instance.
%A set is a mathematical construct to assemble multiple objects in a single instance.

$S = \{a, b, c\}$

\langsection{Axiomes}{Axioms}
%TODO Complete section

\langsubsection{Extensionnalité}{Extensionality}

$\forall A\forall B(\forall X(X \in A \equivalence X \in B) \implies A = B)$

\langsubsection{Spécification}{Specification}
%TODO Complete subsection

\langsubsection{Ensemble vide}{Empty set}

Il existe un ensemble vide noté $\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}

Unite all elements of two given sets into one.

\begin{definition_sq} \label{definition:set_union}
$A \union B := \{x \suchthat (x \in A \lor x \in B)\}$
\end{definition_sq}

Pour des ensembles finis : $\forall (E, F) \in \Cat(\Set)^2, \card{E \union F} = \card{E} + \card{F} - \card{E \intersection F}$

Example :

$n,m \in \N$

$A := \{a_0, \cdots, a_n\}$

$B := \{b_0, \cdots, b_m\}$

$A \union B = \{a_0, \cdots, a_n, b_0, \cdots, b_m\}$

\langsubsection{Schéma de compréhension}{Scheme of replacement}
%TODO Complete subsection

\langsubsection{Infini}{Infinity}
%TODO Complete subsection

\subsection{Power set}
%TODO Complete subsection

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 \suchthat x = 0 \lor p \}$

$B := \{ y \in \Omega \suchthat 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.

\begin{definition_sq} \label{definition:set_intersection}
$A \intersection B := \{x \suchthat (x \in A \land x \in B)\}$
\end{definition_sq}

Pour des ensembles finis : $\forall (E, F) \in \Set^2, \card{E \intersection F} = \card{E} - \card{F} + \card{E \union F}$

Example :

$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 \suchthat (x \in A \land x \notin B)\}$
\end{definition_sq}

Pour des ensembles finis : $\forall (E, F) \in \Set^2, \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 the category \ref{definition:category} of sets \ref{set_theory}.

\subsection{Notation}

$\functiondef{A}{B}$

$\function{f}{x}{f(x)}$

\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}

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}

\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 the category \ref{definition:category} of sets \ref{set_theory}.