Ébauche

main.typ

@@ -0,0 +1,912 @@
+/* Cours de mathématiques fondamendales © 2024 by
+   Valentin Moguérou is licensed under CC BY-SA 4.0 */
+
+#import "@preview/bubble:0.1.0": *
+#import "@preview/ctheorems:1.1.2": *
+#show: thmrules
+
+
+#let emptyset = $diameter$
+#let mapsto = $arrow.bar$
+
+
+#let axiom = thmbox(
+    "axiom",
+    "Axiome",
+    fill: rgb("#ffbcbc")
+)
+#let rule = thmbox(
+    "rule",
+    "Règle",
+    fill: rgb("#e3d9ff")
+)
+
+#let hist = thmbox(
+    "hist",
+    "Note historique",
+    fill: rgb("#fff9d9")
+)
+
+#let theorem = thmbox(
+    "theorem",
+    "Théorème",
+    fill: rgb("#e8e8f8")
+)
+
+#let proposition = thmbox(
+    "theorem",
+    "Proposition",
+    fill: rgb("#e8e8f8")
+)
+
+#let lemma = thmbox(
+    "theorem",            // Lemmas use the same counter as Theorems
+    "Lemme",
+    fill: rgb("#efe6ff")
+)
+#let corollary = thmbox(
+    "corollary",
+    "Corollaire",
+    base: "theorem",      // Corollaries are 'attached' to Theorems
+    fill: rgb("#f8e8e8")
+)
+
+#let definition = thmbox(
+    "definition",         // Definitions use their own counter
+    "Définition",
+    fill: rgb("#e8f8e8")
+)
+
+#let notation = thmbox(
+    "definition",         // Definitions use their own counter
+    "Notation",
+    fill: rgb("#e8f8e8")
+)
+
+#let exercise = thmbox(
+    "exercise",
+    "Exercice",
+    stroke: rgb("#ffaaaa") + 1pt,
+    base: none,           // Unattached: count globally
+).with(numbering: "I")  // Use Roman numerals
+
+// Examples and remarks are not numbered
+#let example = thmplain("example", "Example").with(numbering: none)
+#let remark = thmplain(
+    "remark",
+    "Remarque",
+    inset: 0em
+).with(numbering: none)
+
+// Proofs are attached to theorems, although they are not numbered
+#let proof = thmproof(
+    "proof",
+    "Démonstration",
+    base: "theorem",
+)
+
+#let solution = thmplain(
+    "solution",
+    "Solution",
+    base: "exercise",
+    inset: 0em,
+).with(numbering: none)
+
+
+#show: bubble.with(
+    title: "Cours de mathématiques",
+    subtitle: "En finir avec les « boîtes noires »",
+    author: "Valentin Moguérou",
+    affiliation: "Lycée Saint-Louis",
+    date: datetime.today().display(),
+    year: "2024",
+    class: "MP2I",
+    logo: none,
+) 
+
+// Edit this content to your liking
+
+
+= Module Logique (2h)
+
+== Contexte
+
+On se place dans le cadre de la logique classique du premier ordre, non définie ici. On rappelle informellement ses enjeux ici.
+
+#definition[
+    Une suite de symboles mathématiques s'appelle un *assemblage*. Parmi les assemblages qui ont un sens, on distingue les *termes* et les *relations*. Les termes sont des objets mathématiques, et les relations sont des phrases qui font intervenir ces objets mathématiques.
+
+    L'application de définitions, vues comme raccourcis de langage, permettent, par l'introduction de symboles ou de mots français, de se dispenser d'écrire une pure suite de symboles.
+]
+
+#example[
+    #table(
+        columns: (1fr, 1fr, 1fr),
+        table.header(
+            [*Termes*], [*Relations*], [*Ni l'un, ni l'autre*]
+        ),
+
+        [
+            - $1+1$
+            - $NN$
+            - ${n in ZZ | exists p in ZZ : n=2p+1}$
+        ],
+        [
+            - $1+1=2$
+            - Les zéros non triviaux de la fonction $zeta$ se situent tous sur la droite complexe d'équation $Re (z) = 1/2$.
+            - $2 + 2 = 5$
+        ],
+        [
+            - $1 "et" 2$
+        ]
+
+    )
+]
+
+
+#definition[
+    Les relations font intervenir une ou plusieurs variables. On appelle argument de la relation toute variable non définie présente dans la relation. On appelle arité de la relation son nombre d'arguments.
+
+    On dit qu'une relation est un prédicat si elle est d'arité $>=1$, et que c'est une proposition sinon.
+]
+
+#definition("Vérité")[
+    On attribue aux propositions une valeur booléenne appelée vérité, qui peut être "vrai" ou "faux" : l'un ou l'autre, toujours l'un, mais jamais les deux à la fois.
+
+    Une proposition vraie (resp. fausse) est appelée une tautologie (resp. antilogie).
+
+    On note $top$ (lire "top") et $bot$ (lire "bot") deux propositions telles que $top$ soit vraie et $bot$ soit fausse.
+]
+
+== Connecteurs logiques
+
+#definition("Connecteurs logiques")[
+    Étant donné deux propositions P et Q, on appelle :
+
+    - négation de $P$, notée $not P$, la proposition vraie ssi $not P$ est fausse~;
+    - conjonction de $P$ et $Q$, notée $P and Q$ ou $P "et" Q$, la proposition vraie ssi $P$ et $Q$ sont simultanément vraies~;
+    - disjonction de $P$ et $Q$, notée $P or Q$ ou $P "ou" Q$ la proposition fausse ssi $P$ et $Q$ sont simultanément fausses
+]
+
+On donne les tables de vérité des connecteurs précédents.
+
+
+#figure(grid(columns: 3, row-gutter: 1cm, column-gutter: 1cm,
+
+table(
+    columns: (auto, auto),
+    [$P$], [$not P$],
+    [V], [F],
+    [F], [V]
+),
+
+table(
+    columns: (auto, auto, auto),
+    [$P$], [$Q$], [$P and Q$],
+    [V], [V], [V],
+    [V], [F], [F],
+    [F], [V], [F],
+    [F], [F], [F]
+),
+
+table(
+    columns: (auto, auto, auto),
+    [$P$], [$Q$], [$P or Q$],
+    [V], [V], [V],
+    [V], [F], [V],
+    [F], [V], [V],
+    [F], [F], [F]
+),
+
+"a) Table de la négation", "b) Table de la conjonction", "c) Table de la disjonction"
+),
+
+caption: "Tables de vérités usuelles")
+
+
+
+#definition("Équivalence au sens de la vérité")[
+    On dit que deux propositions $P$ et $Q$ sont équivalentes au sens de la vérité, et l'on note $P equiv Q$ ssi elles ont la même valeur de vérité.
+]
+
+
+#proposition("Propriétés élémentaires des connecteurs logiques")[
+    Soient $P$, $Q$ et $R$ trois propositions. On a toujours~: 
+
+    - $P and Q equiv Q and P$ (commutativité de $and$)
+    - $P or Q equiv Q or P$ (commutativité de $or$)
+    - $(P and Q) and R equiv P and (Q and R)$ (associativité de $and$)
+    - $(P or Q) or R equiv P or (Q or R)$ (associativité de $or$)
+    - $not not P equiv P$ (double négation)
+    - $not (P and Q) equiv not P or not Q$ (lois de De Morgan)
+    - $not (P or Q) equiv not P and not Q$ (lois de De Morgan)
+    - $(P and Q) or R equiv (P or R) and (Q or R)$ (distributivité de $or$ par rapport à $and$)
+    - $(P or Q) and R equiv (P and R) or (Q and R)$ (distributivité de $and$ par rapport à $or$)
+]
+
+#proof[
+    Il suffit de dresser les tables de vérité.
+]
+
+
+#remark[Dualité][
+    Remarquons que les formules présentées restent vraies si l'on change tous les $and$ par des $or$ et inversement.
+]
+
+
+== Implication et équivalence
+
+
+#definition("Implication")[
+    Étant données deux propositions P et Q, on appelle implication de P envers Q, et l'on note $P => Q$, la proposition $not P or Q$.
+]
+
+#figure(
+table(
+    columns: (auto, auto, auto),
+    [$P$], [$Q$], [$P => Q$],
+    [V], [V], [V],
+    [V], [F], [F],
+    [F], [V], [V],
+    [F], [F], [V]
+),
+
+caption: "Table de vérité de l'implication")
+
+
+
+#definition[Soient $P$ et $Q$ deux propositions. On appelle *contraposée* de l'implication $P => Q$ l'implication $not Q => not P$, et *réciproque* de $P => Q$ l'implication $Q => P$.]
+
+#proposition[
+    Une implication et sa contraposée sont équivalentes au sens de la vérité.
+]
+
+#proof[
+    Soient $P$ et $Q$ deux propositions. On a~:
+
+    $ P => Q &equiv not P or Q \
+    &equiv Q or not P  quad &&"(commutativité)" \
+    &equiv not not Q or not P &&"(double négation)" \
+    &equiv not Q => not P $
+]
+
+#definition[
+    On appelle équivalence de $P$ et $Q$, notée $P <=> Q$, la proposition
+    $ (P => Q) and (Q => P) $
+]
+
+#figure(
+table(
+    columns: (auto, auto, auto),
+    [$P$], [$Q$], [$P <=> Q$],
+    [V], [V], [V],
+    [V], [F], [F],
+    [F], [V], [F],
+    [F], [F], [V]
+),
+
+caption: "Table de vérité de l'équivalence")
+
+
+#proposition[
+    Soient P et Q deux propositions. Alors on a $P equiv Q$ si, et seulement si la proposition $P <=> Q$ est vraie.
+]
+
+#proof[
+    - Mq $==>$. Supposons $P equiv Q$. Alors $P$ et $Q$ ont la même valeur de vérité, donc on a~:
+        - Soit $P$ est vraie et $Q$ est vraie, donc $P <=> Q$ est vraie
+        - Soit $P$ est fausse et $Q$ est fausse, donc $P <=> Q$ est fausse
+    - Mq $<==$. Supposons que $P<=>Q$ soit vraie. Alors d'après la table de vérité de l'équivalence, on a soit $P$ vraie et $Q$ vraie, soit $P$ fausse et $Q$ fausse. Dans les deux cas, $P$ et $Q$ ont la même valeur de vérité donc $P equiv Q$.
+]
+
+
+== Raisonnements
+
+#rule[
+    Pour montrer qu'une proposition de la forme $P => Q$ est vraie, on écrit~:
+
+    "Supposons que $P$, montrons $Q$.", puis on démontre $Q$.
+    
+    Formellement, on dit que l'on démontre $Q$ dans la théorie obtenue en adjoignant $P$ aux axiomes de la théorie ambiante.
+]
+
+#proposition(emph("Modus ponens"))[
+    Soient P et Q deux propositions, alors
+    $ P and (P => Q) => Q $ est une tautologie.
+]
+
+#proof[
+    On a d'abord
+    $ P and (P => Q) &equiv P and (not P or Q) \ &equiv (P and not P) or (P and Q) \ &equiv P and Q, $
+    puis $P and Q => Q$, car
+
+    $ P and Q => Q equiv not(P and Q) or Q equiv not P or underbrace(not Q or Q, equiv top) equiv top. $
+]
+
+
+
+
+
+== Quantification
+
+Jusqu'ici nous avons travaillé à l'ordre zéro, c'est-à-dire que nous n'avons travaillé qu'avec des propositions, des relations d'arité zéro. Nous introduisons donc des notions de calcul des prédicats, essentielles.
+
+
+=== Motivation
+
+Si l'on considère $P_1, ..., P_n$ $n$ propositions. On peut se demander s'il existe un $k$ entre $1$ et $n$ tel que $P_k$ soit vraie, et on peut se demander si toutes les propositions $P_k$ sont vraies.
+
+
+En écrivant $ D = P_1 or ... or P_n = or.big_(i=1)^n P_i quad "et" quad C = P_1 and ... and P_n = and.big_(i=1)^n P_i, $
+
+le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite généraliser. On considère un prédicat unaire $P(x)$, d'unique argument $x$. On veut savoir s'il existe un $x$ tel que $P(x)$ ou si pour tout x, on ait $P(x)$. Cependant, on ne peut pas énumérer tous les termes $x$ pour les tester. On est donc limité par nos symboles actuels. On en introduit donc deux autres.
+
+#definition("Quantificateurs")[
+    Soit $P(x)$ un prédicat unaire d'argument $x$.
+
+    On note~:
+    - $exists x P(x)$ la proposition (il s'agit bien d'une proposition) vraie si, et seulement si il existe un terme $x$ tel que $P(x)$.
+    - $forall x P(x)$ la proposition vraie ssi pour tout terme $x$, $P(x)$ soit vraie
+]
+
+#proposition("Négation d'une quantification")[
+    Soit $P(x)$ un prédicat. On a~:
+
+    - $ not( exists x space P(x) ) equiv forall x space not P(x) $
+    - $ not( forall x space P(x) ) equiv exists x space not P(x) $
+]
+
+#remark[C'est une généralisation des lois de De Morgan.]
+
+#proof[
+    
+    - Supposons $not (exists x space P(x))$. Montrons que $forall x space not P(x)$.
+    
+        Soit $x$ un terme, montrons que $P(x)$. Supposons par l'absurde $P(x)$, alors $P(x)$ serait exemplifiée par $x$, donc $exists x space P(x)$ ce qui contredit l'hypothèse.
+    
+    - Supposons $forall x space not P(x)$. Montrons que $not( exists x space P(x) )$. Supposons par l'absurde qu'il existe un $x$ tel que $P(x)$. Alors en applicant l'hypothèse à $x$, on aurait $not P(x)$, ce qui est absurde.
+
+    - Pour le deuxième point, on utilise le premier. On a
+
+    $ not( forall x space P(x) ) equiv not not (exists x space P(x)) equiv exists x space P(x). $
+]
+
+#proposition("Compatibilité des quantificateurs avec les connecteurs idoines")[
+    Soient $P(x)$ et $Q(x)$ deux prédicats unaires. On a
+
+    - $ exists x space (P(x) or Q(x)) equiv (exists x space P(x)) or (exists x space Q(x)) $
+    - $ forall x space (P(x) and Q(x)) equiv (forall x space P(x)) and (forall x space Q(x)) $
+]
+
+#remark[C'est une généralisation de l'associativité de $or$ et $and$.]
+
+#proof[Triviale, laissée en exercice de rédaction au lecteur.]
+
+
+
+= Module Ensembles, relations et applications (2h)
+
+== Vocabulaire ensembliste
+
+#hist[
+    La théorie des ensembles s'est formalisée à la fin du XIX#super[e] siècle avec l'appui de mathématiciens tels que Georg Cantor (1845-1918), David Hilbert (1862-1943). WIP
+]
+
+#definition("Ensemble")[
+    On appelle ensemble tout terme.
+]
+
+#remark[
+    Cette définition paraît décevante au premier regard. On vous avait peut-être vendu précédemment une notion de "collection d'objets mathématiques", ou bien de "collection désordonnée d'objets mathématiques". Mais ces définitions n'en sont pas vraiment, elles utilisent elles-mêmes des mots non définis.
+
+    Ces tentatives de définitions qui plaisent à l'intuition cachent le fait que le concept d'ensemble est une *notion primitive* de la théorie des ensembles. C'est un concept qui n'est pas défini car c'est une brique de base de la théorie.
+]
+
+
+
+#notation[
+    Soit $cal(R)$ une relation binaire. Quels  que soient les termes $x$ et $y$, on note $x cal(R) y$ la proposition $cal(R)(x, y)$.
+]
+
+
+
+#definition("Appartenance")[
+    On considère sur la théorie des ensembles un prédicat binaire noté $in$. Pour tous termes $x, y$, on note $x in y$ au lieu de $op(in)(x, y)$ et l'on dit $x$ appartient à $y$.
+]
+
+
+#notation("Quantification restreinte ou typique")[
+    Soit $P(x)$ un prédicat et $E$ un ensemble.
+
+    On note~:
+    - $exists x in E quad P(x)$ au lieu de $exists x quad x in E and P(x)$~;
+    - $forall x in E quad P(x)$ au lieu de $forall x quad x in E => P(x)$.
+]
+
+#remark[
+    En particulier, *quel que soit* le prédicat $P$,
+    - $exists x in emptyset quad P(x)$ est une antilogie
+    - $forall x in emptyset quad P(x)$ est une tautologie
+]
+
+
+#definition("Égalité")[
+    On définit une relation binaire notée $=$, et l'on note $x = y$ au lieu de $op(=)(x, y)$ et l'on dit que $x$ égale $y$ ou que $x$ et $y$.
+]
+
+#rule("Critères de substitution")[
+    Soit $P(x)$ un prédicat unaire, et $U(x)$, $V(x)$ deux termes à un argument.
+
+    Alors~:
+    - $forall x forall y quad x=y => ( P(x) <=> P(y) )$~;
+    - $forall x quad x = y => U(x) = V(y)$.
+]
+
+== Axiomes de la théorie des ensembles
+
+#axiom("Existence d'un ensemble vide")[
+    Il existe un ensemble vide, c.-à-d.~:
+    $ exists E space forall x quad x in.not E $
+]
+
+#definition[
+    Soient $E$ et $F$ deux ensembles. On dit que $E$ est inclus dans $F$ et l'on note $E subset F$ si, et seulement si
+    $forall x quad x in E => x in F$.
+]
+
+#axiom("Axiome d'extensionnalité")[
+    Les ensembles sont entièrement caractérisés par leurs éléments, c'est-à-dire~:
+
+    $ forall E forall F quad E = F <=> (forall x quad x in E <=> x in F), $
+
+    ce qui est équivalent à
+
+    $ forall E forall F quad E = F <=> (E subset F and F subset E) $
+]
+
+
+
+
+#definition[
+    On dit qu'une relation binaire est~:
+    - réflexive ssi $forall x quad x cal(R) x$
+    - symétrique ssi $forall x forall y quad x cal(R) y => y cal(R) x$
+    - transitive ssi $forall x forall y forall z quad x cal(R) y and y cal(R) z => x cal(R) z$
+    - antisymétrique ssi $forall x forall y quad x cal(R) y and y cal(R) x => x = y $.
+]
+
+
+
+#definition("Relation d'équivalence")[
+    On dit qu'une relation binaire $cal(R)$ est une relation d'équivalence ssi elle est réflexive, symétrique et transitive.
+]
+
+#definition("Relation d'ordre")[
+    On dit qu'une relation binaire $cal(R)$ est une relation d'ordre ssi elle est réflexive, transitive et antisymétrique.
+]
+
+
+#proposition[
+    L'égalité est une relation d'équivalence.
+]
+
+#proof[
+    Elle coïncide avec la relation binaire $cal(R)$ définie pour tous ensembles $E$, $F$ par $E cal(R) F <=> (forall x quad x in E <=> x in F)$ qui est évidemment une relation d'équivalence.
+]
+
+#proposition[
+    L'inclusion est une relation d'ordre.
+]
+
+#proof[
+    - La réflexivité et la transitivité découlent des propriétés de l'implication~;
+    - L'antisymétrie est l'axiome d'extensionnalité.
+]
+
+#proposition[
+    Il existe un unique ensemble vide. On le note $emptyset$.
+]
+
+#proof[
+    - Existence : par axiome
+    - Unicité : Soient $E$ et $F$ deux ensembles tels que $forall x space (x in.not E and x in.not F)$. On a alors $E subset F$ et $F subset E$, donc par l'axiome d'extensionnalité $E = F$.
+]
+
+
+#definition("Quantification existentielle avec unicité")[
+    Soit $P(x)$ un prédicat. On note
+    $ exists! x quad P(x) $
+    la proposition
+    $ ( exists x quad P(x) ) and (forall x forall y space P(x) and P(y) => x=y) $
+]
+
+
+#definition[
+    On dit qu'un prédicat $P$ de variable $x$ est collectivisant en $x$ si, et seulement si
+
+    $ exists E space forall x quad (x in E <=> P(x)). $
+]
+
+#proposition[
+    Dans ce cas, si un ensemble $E$ vérifie $ forall x quad x in E <=> P(x), $ alors il est unique et on le note ${ x | P(x) }$.
+]
+
+#proof[
+    Soient $E$ et $F$ deux ensembles, dont l'appartenance équivaut à vérifier $P$. Alors, pour tout $x$, $x in E <=> P(x) <=> x in F$ donc par l'axiome d'extensionnalité, $E=F$.
+]
+
+#axiom("Schéma d'axiomes de compréhension")[
+    Soit $P$ un prédicat unaire et $E$ un ensemble. Alors la relation $x in E and P(x)$ est collectivisante en $x$.
+]
+
+#notation[
+    On note ${x in E | P(x)} = {x | x in E and P(x)}$
+]
+
+
+#proposition[Intersection binaire][
+    Soient $A$ et $B$ deux ensembles. Alors la relation $x in A and x in B$ est collectivisante en $x$. L'ensemble associé est noté $A sect B$.
+]
+
+
+#proof[
+    Il suffit de poser $A sect B = {x in A | x in B}$.
+]
+
+
+#proposition[Intersection quelconque][
+    Soit $E$ un ensemble *non vide*. Alors la relation $forall F in E, x in F$ est collectivisante en $x$. L'ensemble associé se note alors $sect.big E$ ou encore $display(sect.big_(F in E) E)$.
+]
+
+#proof[
+    Comme $E$ est non vide, il possède un élément $F_0$. On pose alors $ I = { x in F_0 | forall F in E, x in F }. $
+
+    On a alors, pour tout $x$~:
+
+    $ x in I &<=> x in F_0 and forall F in E quad x in F \
+    &<=> forall F in E quad x in F quad "car" F_0 in E $
+]
+
+#proposition[Différence ensembliste][
+    Soient $A$ et $B$ deux ensembles. Alors la relation $x in A and not (x in B)$ est collectivisante en $x$. L'ensemble associé est noté $A without B$.
+]
+
+
+#proof[
+    Il suffit de poser $A without B = {x in A | x in.not B}$.
+]
+
+#definition[Complémentaire][
+    En particulier, quand $B$ est une partie de $A$, on note $complement_A B$ ou $overline(B)^A$, ou $overline(B)$ lorsqu'il n'y a pas d'ambiguïté sur la valeur de $A$, l'ensemble $A without B$, et on l'appelle le complémentaire de B dans A.
+]
+
+
+#axiom("Axiome de la paire")[
+    Soient $a$ et $b$ deux termes (non nécessairement différents). Alors la relation $x = a or x = b$ est collectivisante en $x$. L'ensemble associé se note ${a; b}$.
+]
+
+#remark[
+    En particulier, cet axiome assure que pour tout $a$, le singleton ${a}$ existe. On a donc par définition
+    $ forall x quad x in {a} <=> x = a. $
+]
+
+#axiom("Axiome de l'union")[
+    Soit $E$ un ensemble (comprendre ensemble d'ensembles). Alors la relation
+    $ exists F in E quad x in F $
+    est collectivisante en $x$. L'ensemble associé se note $union.big E$ ou $display(union.big_(F in E) F)$.
+]
+
+
+#proposition[Union binaire][
+    Soient $A$ et $B$ deux ensembles. La relation $x in A or x in B$ est collectivisante en $x$ et l'on note $A union B$ l'ensemble associé.
+]
+
+#proof[
+    Il suffit de poser $A union B = union.big {A; B}. $
+]
+
+// TODO
+#proposition[Traductions ensemblistes ][
+    Soit 
+]
+
+
+#axiom[Axiome des parties][
+    Soit $E$ un ensemble. Alors la relation $F subset E$ est collectivisante en $F$. L'ensemble associé se note $cal(P)(F)$ ou $frak(P)(F)$.
+]
+
+
+#axiom[Axiome de fondation][
+    Soit $E$ un ensemble non vide. Alors il possède un élément $x$ tel que $x sect E = emptyset$.
+]
+
+
+#proposition[Irréflexivité de l'appartenance][
+    Soit $E$ un ensemble. Alors $E in.not E$.
+]
+
+
+#proof[
+    Soit $E$ un ensemble. Supposons par l'absurde $E in E$. On a donc ${E} subset E$. Comme ${E}$ est non vide, il possède un élément $x$ tel que $x sect E = emptyset$. Or $x in {E}$ donc $x = E$, puis $E sect E = emptyset$, donc $E = emptyset$, ce qui contredit le fait qu'il possède un élément.
+]
+
+
+
+== Couples
+
+#definition("Couples au sens de Kuratowski")[
+    Soient $x$ et $y$ deux termes. On appelle couple formé de $x$ et $y$ l'ensemble ${{x}; {x; y}}$. On le note $(x; y)$.
+]
+
+#proposition("Unicité des couples")[
+    Soient $a$, $b$, $c$, $d$ quatre termes. On a~:
+
+    $ (a; b) = (c; d) <=> cases(a=c \ b=d) $
+]
+
+#proof[
+    Par double implication.
+    
+    L'implication $<==$ est évidente. Montrons $==>$.
+
+    Supposons $(a, b) = (c,d)$. Montrons $a=c$ et $b=d$.
+
+    On a donc ${{a}; {a; b}} = {{c}; {c; d}}$,
+
+    donc
+
+    - Ou bien ${a} = {c; d}$ et ${a; b} = {c}$, ce qui implique $a=b$ et $c=d$, puis $a=c$ et $a=d$
+    - Ou bien ${a} = {c}$ et ${b} = {d}$, donc $a=c$ et $b=d$.
+]
+
+
+#definition[
+    Pour tout couple $(a, b)$, on note $op("pr"_1)((a, b)) = a$ et $op("pr"_2)((a, b)) = b$.
+]
+
+Ces deux opérateurs sont bien définis par la propriété précédente.
+
+#notation[
+    Si $P(x,y)$ est un prédicat binaire, au lieu de $forall x forall y quad P(x, y)$ on peut noter $forall (x; y) quad P(x; y)$.
+]
+
+#definition[
+    Soit $cal(R)$ une relation binaire. On dit que $cal(R)$ est collectivisante si, et seulement si la relation "$x$ est un couple de la forme $(a, b)$ et $cal(R)(a; b)$" est collectivisante en $x$.
+
+    Dans le cas où $cal(R)$ est collectivisante, l'ensemble associé s'appelle *graphe* de $cal(R)$.
+]
+
+#proposition("Produit cartésien")[
+    Soient $E$ et $F$ deux ensembles.
+    
+    La relation $x in E and y in F$ est collectivisante en $(x, y)$.
+    
+    On appelle produit cartésien de $E$ et $F$, noté $E times F$ et lu "E croix F" l'ensemble associé.
+]
+
+#proof[
+    On cherche à trouver un surensemble de l'ensemble que l'on essaie de construire, pour en prendre une partie.
+
+    Soit $x in E$ et $y in F$. On a $(x, y) = {{x}, {x, y}} = {{x}} union {{x, y}}.$
+
+    Or $x in E$ et $y in F$ donc ${x, y} subset E union F$ puis ${x, y} in cal(P)(E union F)$. De même ${x} in cal(P)(E union F)$, puis ${{x}, {x, y}} in cal(P)(cal(P)(E union F))$.
+
+    Pour tout $a$, notons $P(a)$ la proposition "$a$ est un couple de la forme $(x, y)$ et $x in E and y in F$)".
+
+    On a montré $forall a quad P(a) => a in cal(P)(cal(P)(E union F))$.
+
+    Notons $G = { a in cal(P)(cal(P)(E union F))  | P(a)}.$
+
+    On a toujours $forall a quad P(a) => a in G$ mais on a en plus $forall a quad a in G => P(a)$, donc la relation $P(a)$ est collectivisante en $a$ d'ensemble associé $G$.
+]
+
+
+
+== Correspondances et applications
+
+
+#definition("Correspondance")[
+    Soient $E$ et $F$ deux ensembles, et $Gamma subset E times F$. On appelle correspondance entre $E$ et $F$ le terme $f = (Gamma, (E, F))$.
+
+    On note $op("Cor")(E, F)$ l'ensemble des correspondances de $E$ vers $F$. Il s'agit bien d'un ensemble car il s'identifie naturellement à $cal(P)(E times F)$.
+
+    On note $x mapsto y$ la relation $(x, y) in Gamma$.
+
+    On dit que $E$ est l'ensemble de départ de $f$ et que $F$ est l'ensemble d'arrivée de $f$.
+
+    Pour tout $(x, y) in E times F$, si $x mapsto y$ on dit que $y$ est une image de $x$ et que $x$ est un antécédent de $x$.
+]
+
+#definition("Fonction")[
+    Soit $E$, $F$ deux ensembles et $f$ une correspondance de $E$ vers $F$. On dit que $f$ est une fonction de $E$ dans $F$ si, et seulement si
+
+    $ forall x in E space forall(y, y') in F^2 quad ( x mapsto y and x mapsto y' ) => y=y' $
+
+    Cela revient à dire que si un élément $x$ de $E$ possède une image, alors elle est unique. On la note alors $f(x)$.
+]
+
+#definition("Application")[
+    Soit $E$, $F$ deux ensembles et $f$ une correspondance de $E$ vers $F$. On dit que $f$ est une application de $E$ dans $F$ si, et seulement si
+
+    $ forall x in E space exists !y in F quad x mapsto y. $
+
+    Cela revient à dire que tout élément de $E$ possède une image et qu'elle est unique. On la note alors $f(x)$.
+    L'ensemble des applications de E dans F se note $F^E$ (ou plus rarement $cal(F)(E, F)$).
+]
+
+#definition("Injectivité, surjectivité, bijectivité")[
+    Soit $f$ une application de $E$ dans $F$. On dit qu'elle est~:
+    - injective ssi $forall (x, x') in E^2 quad f(x) = f(x') => x=x'$
+    - surjective ssi $forall y in F space exists x in E quad f(x) = y$
+    - bijective ssi elle est injective et surjective
+]
+
+#proposition("Caractérisation des bijections")[
+    Soit $f$ une application de $E$ dans $F$. Elle est bijective si, et seulement si
+
+    $ forall y in F space exists! x in E quad f(x) = y. $
+]
+
+#definition("Permutation")[
+    Soit $E$ un ensemble. Une bijection de $E$ dans $E$ s'appelle une permutation.  L'ensemble des permutations de $E$ se note $S(E)$ ou $frak(S)(E)$
+]
+
+#definition[Identité][
+    Pour tout ensemble $E$, on note $id_E$ l'application
+
+    $ id_E : E &-> E \
+    x &|->x $
+]
+
+#definition[Composition][
+    Soient $E$, $F$, $G$ trois ensembles et $f: E -> F$, $g: F -> G$ deux applications. On note $ g compose f : E &-> G \ x &|-> g(f(x)). $
+
+    Attention, c'est la fonction $f$ qui est évaluée en premier.
+]
+
+Attention, la proposition suivante est réservée pour une seconde lecture et fait appel à des notions encore non abordées.
+
+#proposition[Structure de $S_E$][
+    Soit $E$ un ensemble. $(S_E, compose)$ est un groupe.
+]
+
+
+#definition[Image directe][
+    Soit $E$, $F$ deux ensembles, $f$ une application de $E$ dans $F$ et $A$ une partie de $E$. On appelle image directe de $A$ par $f$, notée $f(A)$ l'ensemble
+
+    $ {y in F | exists x in E space f(x)=y} $
+]
+
+#proposition[
+    Soit $E$, $F$ deux ensembles, $f$ une application de $E$ dans $F$ et $A$, $B$ deux parties de $E$. On a~:
+
+    - $f(A union B) subset f(A) union f(B)$
+    - $f(A sect B) subset f(A) sect f(B)$
+    - $overline(f(A)) subset f(overline(A))$
+]
+
+#notation[
+    On le note aussi 
+    ${f(x) : x in E}.$ Cette dernière notation permet de ne pas expliciter l'application $f$ mais seulement son comportement.
+]
+
+#definition[Image réciproque][
+    Soit $E$, $F$ deux ensembles, $f$ une application de $E$ dans $F$ et $B$ une partie de $F$. On appelle image réciproque de $B$ par $f$, notée $f^(-1)(B)$ l'ensemble
+    $ { x in E | f(x) in B }. $
+]
+
+
+== Entiers naturels
+
+#definition[Opérateur "successeur"][
+    Pour tout ensemble $E$, on appelle successeur de $E$, noté $s(E)$ l'ensemble $E union {E}$.
+]
+
+#definition[
+    On note~: $0 := emptyset$, $1 := s(emptyset)$, $2 := s(s(emptyset))$, $3 := s(s(s(emptyset)))$, ...
+]
+
+#proposition[
+    On a toujours $E subset s(E)$.
+]
+#proof[Triviale.]
+
+#proposition[
+    Soit $E$ un ensemble. L'union $E union {E}$ est disjointe.
+]
+
+#proof[
+    Soit $E$ un ensemble. Supposons par l'absurde $E union {E} != emptyset$. Il existe donc $x in E union {E}$ puis $x = E$ donc $E in E$, ce qui est absurde.
+]
+
+#proposition[Fondation][
+    L'ensemble vide n'a pas de prédecesseur.
+]
+
+#proof[
+    Supposons qu'il existe un ensemble $E$ tel que $s(E) = emptyset$. Alors $E subset emptyset$ donc $E = emptyset$.
+]
+
+
+#definition[
+    On dit qu'un ensemble $E$ est héréditaire si, et seulement si
+    $ forall x in E quad s(x) in E. $
+]
+
+#definition[
+    Soit $E$ un ensemble héréditaire. On appelle support de $E$, noté $op("Supp")(E)$ l'ensemble $ { y in E | forall x in E space s(x) != y }. $
+
+    C'est le sous-ensemble des éléments de $E$ qui n'ont pas de prédecesseur.
+]
+
+
+
+/*
+#proposition[
+    Soit $E$ un ensemble IH et $X in E$. Alors il existe $B in op("Supp")(E)$ tel que $B subset X$.
+]
+
+#proof[
+    Soit $E$ IH et $X in E$. Supposons par l'absurde que pour tout $B in op("Supp")(E), B subset.not X$. Ainsi, pour tout $B in op("Supp")(E)$, $B without X$ est non vide.
+]
+
+#proposition[
+    Soient $E$ et $F$ deux ensembles IH. Alors $E subset F$ si, et seulement si $op("Supp") E subset op("Supp") F$.
+]
+
+#proof[
+    Supposons $E subset F$. Montrons que 
+]
+
+#proposition[
+    Soient $E$ et $F$ deux ensembles initalement héréditaires. Alors ils sont égaux si, et seulement si leurs supports sont égaux.
+]
+
+#proof[
+    Par antisymétrie~!
+]
+
+
+/*
+#proposition[Unicité de l'ensemble des entiers naturels][
+    Disons qu'un ensemble $E$ vérifie la propriété H si, et seulement si $emptyset in E and forall x in E, s(x) in E $.
+
+    Alors il existe un unique ensemble $E$ tel que pour tout ensemble $F$, si $F$ vérifie la propriété $H$ alors $E subset F$.
+]
+
+#proof[
+    Par l'axiome de l'infini, il existe un ensemble qui vérifie la propriété H. Notons-le $H_0$. Notons $cal(H) = {H in cal(P)(H_0) | H "vérifie la propriété H" }$. Considérons
+    $ E = sect.big_(H in cal(H)) H. $
+
+    Montrons que E vérifie la propriété H.
+
+    - On a $forall H in cal(H), emptyset in H$, donc $emptyset in E$~;
+    - Soit $x in E$. Montrons que $s(x) in E$. On a $forall x in cal(H), x in H$ donc en appliquant la propriété H à chacun des éléments de $cal(H)$, on obtient $forall H in cal(H), s(x) in H$, donc $s(x) in E$.
+
+    Montrons que pour tout ensemble $F$, si $F$ vérifie la propriété $H$ alors $E subset F$.
+
+    Soit $F$ un ensemble qui vérifie la propriété $H$. Montrons que $E subset F$. Soit $x in E$ et montrons que $x in F$.
+
+    On considère
+]
+*/
+*/
+
+
+#proposition[Source d'un élément][
+    Soit E un ensemble héréditaire, et $x in E$.
+]
+
+#axiom[De l'infini][
+    Il existe un ensemble héréditaire qui possède $emptyset$.
+]
+
+Attention, un tel ensemble n'a pas de raison d'être unique~! En effet, on pourrait très bien imaginer un ensemble constitué de deux chaînes distinctes~:
+
+$ E_("hyp") = { emptyset, s(emptyset), s^2 (emptyset), ..., alpha, s(alpha), ...} $
+
+On voudrait donc bien disposer d'un ensemble unique, qui ne possède qu'une seule chaîne~!
+
+#proposition[Ensemble des entiers naturels][
+    Il existe un unique ensemble héréditaire de support ${emptyset}$. On le note $NN$.
+]