diff --git a/main.pdf b/main.pdf index 8c8db1d..63dceac 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.typ b/main.typ index 82b77e8..7d38a2d 100644 --- a/main.typ +++ b/main.typ @@ -1,11 +1,29 @@ /* 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/bubble:0.1.0": * #import "@preview/ctheorems:1.1.2": * #show: thmrules +#let bw = false; +#let friendly = false; + +#let main-font = if friendly { "Montserrat" } else { "New Computer Modern" } +#let title-font = if friendly { "Montserrat" } else { "DejaVu Sans" } + +#set par(justify: true) +#set text( + font: main-font, + size: 11pt, +) + +#if friendly { + show math.equation: set text( + font: "Fira Math", + ) +} + #let emptyset = $diameter$ #let mapsto = $arrow.bar$ @@ -13,54 +31,63 @@ #let axiom = thmbox( "axiom", "Axiome", - fill: rgb("#ffbcbc") + fill: if bw {none} else {rgb("#ffbcbc")}, + stroke: if bw {1.5pt} else {none}, ) #let rule = thmbox( "rule", "Règle", - fill: rgb("#e3d9ff") + fill: if bw {none} else {rgb("#ffd8a2")}, + stroke: if bw {1.5pt} else {none}, ) #let hist = thmbox( "hist", "Note historique", - fill: rgb("#fff9d9") + fill: if bw {none} else {rgb("#fff9d9")}, + stroke: if bw {.5pt} else {none}, ) #let theorem = thmbox( "theorem", "Théorème", - fill: rgb("#e8e8f8") + fill: if bw {none} else {rgb("#e3d9ff")}, + stroke: if bw {1.5pt} else {none}, ) #let proposition = thmbox( "theorem", "Proposition", - fill: rgb("#e8e8f8") + fill: if bw {none} else {rgb("#e8e8f8")}, + stroke: if bw {1pt} else {none}, ) #let lemma = thmbox( "theorem", // Lemmas use the same counter as Theorems "Lemme", - fill: rgb("#efe6ff") + fill: if bw {none} else {rgb("#efe6ff")}, + stroke: if bw {.5pt} else {none}, ) #let corollary = thmbox( "corollary", "Corollaire", base: "theorem", // Corollaries are 'attached' to Theorems - fill: rgb("#f8e8e8") + fill: if bw {none} else {rgb("#f8e8e8")}, + stroke: if bw {.5pt} else {none}, ) #let definition = thmbox( "definition", // Definitions use their own counter "Définition", - fill: rgb("#e8f8e8") + fill: if bw {none} else {rgb("#c4ffcb")}, + stroke: if bw {1pt} else {none}, ) #let notation = thmbox( "definition", // Definitions use their own counter "Notation", - fill: rgb("#e8f8e8") + fill: if bw {none} else {rgb("#e8f8e8")}, + stroke: if bw {.5pt} else {none}, ) #let exercise = thmbox( @@ -71,7 +98,7 @@ ).with(numbering: "I") // Use Roman numerals // Examples and remarks are not numbered -#let example = thmplain("example", "Example").with(numbering: none) +#let example = thmplain("example", "Exemple").with(numbering: none) #let remark = thmplain( "remark", "Remarque", @@ -92,7 +119,7 @@ inset: 0em, ).with(numbering: none) - +/* #show: bubble.with( title: "Cours de mathématiques", subtitle: "En finir avec les « boîtes noires »", @@ -103,20 +130,95 @@ class: "MP2I", logo: none, ) - -// Edit this content to your liking +*/ -= Module Logique (2h) +#let title="Cours de mathématique moderne" +#let author="Valentin Moguérou" +#let date=datetime.today() + +#set document( + title: title, + author: author, + date: date +) + +#v(2fr) +#align(center, { + set text(weight: 700, 20pt) + title + v(1em) + set text(15pt) + author + +}) +#v(4fr) + + +#pagebreak() +#outline( + title: [Table des matières], + indent: auto, + depth: 2, +) + +#set heading(numbering: "1.") +#show heading: it => { + let num = counter(heading).display(it.numbering) + + if counter(heading).get().len() == 1 { + pagebreak() + place(top + left, + circle(radius: 2cm, + fill: if bw { + gradient.radial(luma(196), luma(64)) + } else { + gradient.radial(red, rgb(64, 0, 0)) + }, + [ + #set align(center + horizon) + #set text(font: title-font, size: 4em, fill: luma(255)) + #counter(heading).get().first() + ] + )) + + block( + height: 4cm, + { + v(1fr) + set par(justify: false) + pad( + left: 5cm, + text(font: title-font, size: 1.2em, hyphenate: false, it.body) + ) + v(1fr) + } + ) + } else { + set par(justify: false) + set text(font: title-font, size: 1.5em) + v(1cm) + [ #num #it.body ] + } +} + + += Logique == Contexte -On se place dans le cadre de la logique classique du premier ordre, non définie ici. On rappelle informellement ses enjeux ici. +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. + 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. + 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[ @@ -145,17 +247,29 @@ On se place dans le cadre de la logique classique du premier ordre, non définie #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. + 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. + On dit qu'une relation est un prédicat si elle est d'arité $>=1$, et que c'est + une proposition sinon. +] + +#example[ + - $1+1 = 2$ est une proposition + - $1+x=3$ est un prédicat de variable $x$ + - $x + y = z$ est un prédicat d'arité 3. + - Si la variable $x$ est fixée, alors $1 + x = 2$ est une proposition. ] #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. + 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. + On note $top$ (lire "top") et $bot$ (lire "bot") deux propositions telles que + $top$ soit vraie et $bot$ soit fausse. ] == Connecteurs logiques @@ -206,7 +320,8 @@ 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é. + 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é. ] @@ -230,7 +345,8 @@ caption: "Tables de vérités usuelles") #remark[Dualité][ - Remarquons que les formules présentées restent vraies si l'on change tous les $and$ par des $or$ et inversement. + Remarquons que les formules présentées restent vraies si l'on change tous les + $and$ par des $or$ et inversement. ] @@ -238,7 +354,8 @@ caption: "Tables de vérités usuelles") #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$. + É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( @@ -255,7 +372,9 @@ 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$.] +#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é. @@ -289,13 +408,14 @@ 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. + 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 + - Soit $P$ est fausse et $Q$ est fausse, donc $P <=> Q$ est vraie - 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$. ] @@ -307,39 +427,66 @@ caption: "Table de vérité de l'équivalence") "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. + 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"))[ +#proposition[_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, $ + $ 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. $ + $ P and Q => Q equiv not(P and Q) or Q equiv not P or underbrace(not Q or Q, + equiv top) equiv top. $ ] +#proposition[Disjonction de cas][ + Soient $P$, $Q$ et $R$ trois propositions, alors + $ [ (P or Q) and (P => R) and (Q => R) ] => R $ + est une tautologie. +] +#proof[Exercice.] +#proposition[Démonstration par l'absurde][ + Soit $P$ une proposition. Alors + $ (not P => bot) => P $ + est une tautologie. +] + +#proof[ + On a $not P => bot space equiv space P or bot space equiv space P$, et $P => P$ + est une tautologie. +] + +#corollary[ + En particulier, si de plus $Q$ est une proposition alors + $ (not P => (Q and not Q)) => P $ est une tautologie. +] == 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. +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. + +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. -=== Motivation +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, $ -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. +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$. @@ -362,13 +509,16 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite - 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. + 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. + - 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). $ + $ 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")[ @@ -378,18 +528,20 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite - $ forall x space (P(x) and Q(x)) equiv (forall x space P(x)) and (forall x space Q(x)) $ ] +#proof[Laissée en exercice de rédaction au lecteur.] + #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) += Ensembles, relations et applications == 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 + 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")[ @@ -397,21 +549,29 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite ] #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. + 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. + 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)$. + 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$. + 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$. ] @@ -431,7 +591,8 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #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$. + 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")[ @@ -449,40 +610,55 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite $ exists E space forall x quad x in.not E $ ] +#remark[ + En réalité, cet axiome n'est pas vraiment nécessaire puisqu'on peut l'obtenir + en applicant le schéma d'axiomes de compréhension à l'axiome de l'infini (voir + plus loin). +] + #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 + 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~: + Si deux ensembles ont les mêmes éléments, alors ils sont égaux, c'est-à-dire~: - $ forall E forall F quad E = F <=> (forall x quad x in E <=> x in F), $ + $ forall E forall F quad (forall x quad x in E <=> x in F) => E = F, $ ce qui est équivalent à - $ forall E forall F quad E = F <=> (E subset F and F subset E) $ + $ forall E forall F quad (E subset F and F subset E) => E = F $ +] + +#remark[ + Ce sont évidemment des équivalences. ] - #definition[ - On dit qu'une relation binaire est~: + On dit qu'une relation binaire (resp. sur $E$) 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$ + - 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 $. + + Respectivement, quantifier sur $E$. ] #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. + On dit qu'une relation binaire $cal(R)$ est une relation d'équivalence (resp. sur $E$) ssi elle + est réflexive, symétrique et transitive (resp. sur $E$). ] #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. + On dit qu'une relation binaire $cal(R)$ est une relation d'ordre (resp. sur $E$) ssi elle est + réflexive, transitive et antisymétrique (resp. sur $E$). ] @@ -491,7 +667,9 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite ] #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. + 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[ @@ -509,7 +687,9 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #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$. + - 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$. ] @@ -522,30 +702,46 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #definition[ - On dit qu'un prédicat $P$ de variable $x$ est collectivisant en $x$ si, et seulement si + 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) }$. + 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$. + 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$. + 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[ + Soit $P(x)$ un prédicat. + Si il existe $E$ un ensemble tel que $ forall x quad P(x) => x in E $ + alors $P(x)$ est collectivisant. +] + +#proof[ + Dans ce cas, $P(x) <=> P(x) and x in E$, qui est collectivisant par le schéma + d'axiomes de compréhension. +] #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$. + 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$. ] @@ -555,11 +751,14 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #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)$. + 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 }. $ + 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$~: @@ -568,7 +767,8 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite ] #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$. + 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$. ] @@ -577,28 +777,53 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite ] #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. + 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. +] + + +#theorem[Paradoxe de Russel][ + La relation $top$ n'est pas collectivisante. Autrement dit, il n'existe pas + d'ensemble de tous les ensembles. +] + +#proof[ + Supposons par l'absurde qu'il existe un ensemble $Omega$ tel que $ forall x quad + x in Omega. $ + + Considérons $A = { E in Omega | E in.not E }$. A-t-on $Omega in A$ ? + + - Si oui, alors on aurait $Omega in Omega$ et $Omega in.not Omega$ absurde + - Si non, alors on aurait $Omega in.not Omega$ mais $Omega in Omega$, absurde. + + Ainsi l'ensemble $A$ est mal défini, ce qui contredit le schéma d'axiomes de + compréhension. ] #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}$. + 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 + 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)$. + 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é. + 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[ @@ -612,12 +837,15 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #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)$. + 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)$. ] +On ajoute également cet axiome qui nous servira plus tard~: #axiom[Axiome de fondation][ - Soit $E$ un ensemble non vide. Alors il possède un élément $x$ tel que $x sect E = emptyset$. + Soit $E$ un ensemble non vide. Alors il possède un élément $x$ tel que + $x sect E = emptyset$. ] @@ -627,21 +855,30 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite #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. + 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. ] - +#corollary[Autre version du paradoxe de Russel][ + Il n'existe pas d'ensemble de tous les ensembles. +] +#proof[ + Il se contiendrait lui-même, ce qui est absurde. +] == 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)$. + 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) $ + $ (a, b) = (c, d) <=> cases(a=c \ b=d) $ ] #proof[ @@ -651,29 +888,35 @@ le problème se ramène à la vérité de $D$ ou de $C$. Maintenant on souhaite Supposons $(a, b) = (c,d)$. Montrons $a=c$ et $b=d$. - On a donc ${{a}; {a; b}} = {{c}; {c; 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, 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$. + 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)$. + 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$. + 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)$. + Dans le cas où $cal(R)$ est collectivisante, l'ensemble associé s'appelle *graphe* + de $cal(R)$. ] #proposition("Produit cartésien")[ @@ -681,23 +924,30 @@ Ces deux opérateurs sont bien définis par la propriété précédente. 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é. + 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. + 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))$. + 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$)". + 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$. + 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$. ] @@ -706,32 +956,51 @@ Ces deux opérateurs sont bien définis par la propriété précédente. #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))$. + 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 $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$. + 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$. + 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 + 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' $ + $ 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)$. + 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)$. +] + +#example[ + ($RR$ défini plus loin) $f : x mapsto 1/x$ de $RR$ dans $RR$, mais seulement + définie sur $RR^*$. ] #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 + 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)$). + 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)$). +] + +#example[ + $f: E -> cal(P)(E), x mapsto {x}$. ] #definition("Injectivité, surjectivité, bijectivité")[ @@ -741,14 +1010,22 @@ Ces deux opérateurs sont bien définis par la propriété précédente. - bijective ssi elle est injective et surjective ] +#example[ + - $f: RR_+ -> RR, x mapsto x^2$ est injective~; + - $f: RR -> RR_+, x mapsto x^2$ est surjective~; + - $f: RR_+ -> RR_+, x mapsto x^2$ est bijective. +] + #proposition("Caractérisation des bijections")[ - Soit $f$ une application de $E$ dans $F$. Elle est bijective si, et seulement si + 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)$ + 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é][ @@ -759,12 +1036,14 @@ Ces deux opérateurs sont bien définis par la propriété précédente. ] #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)). $ + 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. +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. @@ -772,13 +1051,15 @@ Attention, la proposition suivante est réservée pour une seconde lecture et fa #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 + 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~: + 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)$ @@ -787,46 +1068,63 @@ Attention, la proposition suivante est réservée pour une seconde lecture et fa #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. + ${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 + 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 += Entiers naturels + +== Succession et ensembles héréditaires #definition[Opérateur "successeur"][ - Pour tout ensemble $E$, on appelle successeur de $E$, noté $s(E)$ l'ensemble $E union {E}$. + Pour tout ensemble $E$, on appelle successeur de $E$, noté $s(E)$ l'ensemble + $E union {E}$. + On dit également que $E$ est un prédecesseur de $s(E)$. ] #definition[ - On note~: $0 := emptyset$, $1 := s(emptyset)$, $2 := s(s(emptyset))$, $3 := s(s(s(emptyset)))$, ... + On note~: $0 := emptyset$, $1 := s(emptyset)$, $2 := s(s(emptyset))$, + $3 := s(s(s(emptyset)))$, ... ] #proposition[ - On a toujours $E subset s(E)$. + On a toujours $E subset s(E)$ et $E in s(E)$. ] -#proof[Triviale.] +#proof[Par définition] #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. + 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][ +#proposition[ 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$. + Supposons qu'il existe un ensemble $E$ tel que $s(E) = emptyset$. Alors + $E subset emptyset$ donc $E = emptyset$, or $s(emptyset) = {emptyset}$, ce qui est absurde. ] +#proposition[Unicité du prédecesseur][ + Soient $E$ et $F$ deux ensembles tels que $s(E) = s(F)$. Alors $E = F$. +] + +#proof[ + à faire +] #definition[ On dit qu'un ensemble $E$ est héréditaire si, et seulement si @@ -834,79 +1132,274 @@ Attention, la proposition suivante est réservée pour une seconde lecture et fa ] #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. + On dit qu'un ensemble $E$ est initialement héréditaire + (IH) si, et seulement si $E$ est héréditaire et $emptyset in E$. ] - -/* -#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$. + Une intersection non vide d'ensembles IH est IH. ] #proof[ - Supposons $E subset F$. Montrons que + Soit $cal(H)$ un ensemble non vide d'ensembles IH. Montrons que + $ sect.big_(H in cal(H)) H quad "est IH". $ + + On a $forall H in cal(H), emptyset in H$ donc $emptyset in cal(H)$. + Soit $x in limits(sect.big)_(H in cal(H))$. Ainsi $forall H in cal(H), x in H$. + Or comme tous les éléments de $cal(H)$ sont IH, on a $forall H in + cal(H), s(x) in H$, puis $s(x) in limits(sect.big)_(H in cal(H))$. ] -#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$. + Il existe un ensemble initialement héréditaire. ] -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~: +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~! +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$. -] \ No newline at end of file + +== Entiers naturels + +#theorem[ + Il existe un unique ensemble appelé *ensemble des entiers naturels* + et noté $NN$, tel que + + $ NN "est IH" quad and quad forall E quad E "est IH" => NN subset E. $ +] + +#proof[ + Posons $P(H)$ le prédicat défini par $ forall E quad E "est IH" + => H subset E. $ + + *Unicité~:* + + Soient $H$, $H'$ deux ensembles tels que $P(H)$ et $P(H')$. + Montrons que $H = H'$. + + On a déjà $H$ IH et $H'$ IH. Ainsi, comme $P(H)$ et $P(H')$ on a~: + $ H subset H' quad and quad H' subset H $ + puis $H = H'$. + + *Existence~:* + + Par l'axiome de l'infini, il existe $H_0$ IH. Considérons + $ H_1 = sect.big_(H in cal(P)(H_0) \ H "est IH") H. $ + + $H_1$ est IH comme intersection d'ensembles IH. Montrons que $P(H_1)$. + + Soit $E$ IH. Montrons que $H_1 subset E$. On a par définition + + $ E sect H_1 = E sect sect.big_(H in cal(P)(H_0) \ H "est IH") H $ + + Or $H_0$ est dans l'intersection, on le sort donc~: + $ E sect H_1 = (E sect H_0) sect sect.big_(H in cal(P)(H_0) \ H "est IH") H $ + + Or $E$ IH et $H_0$ IH, donc $E sect H_0$ IH, donc on + le fait rentrer dans l'intersection, ainsi~: + $ E sect H_1 = sect.big_(H in cal(P)(H_0) \ H "est IH") H = H_1. $ + + Ainsi, on a bien $H_1 subset E$. Le prédicat $P$ est donc exemplifié par $H_1$. +] + +#notation[ + On note $NN^* = NN without {0}$. +] + +#proposition[ + Tout entier naturel $n$ non nul possède un unique prédecesseur que l'on notera $p(n)$. +] + +#proof[ + L'unicité a déjà été démontrée. + + Supposons par l'absurde qu'il existe $n_0 in NN^*$ tel que $ forall n in NN quad s(n) != n_0. $ + + Montrons que $NN without { n_0 }$ est IH. + + - On a $emptyset in NN without {n_0}$ car $n_0 != 0$~; + - Pour tout $n in NN without {n_0}$, on a $s(n) != n_0$, donc $s(n) in NN without {n_0}$. + + Ainsi $NN without {n_0}$ est IH. Or $NN without {n_0} limits(subset)_eq.not NN$, ce qui contredit le théorème précédent. +] + +#proposition[ + Soit $A subset NN$ non vide. Alors $limits(sect.big)_(x in A) x in A$ et + $limits(union.big)_(x in A) x in A$. +] + +#proof[ + à faire +] + +#corollary[ + La relation $subset$ définit une relation d'*ordre total* sur $NN$. On la note + alors $lt.eq.slant$. +] + +#proof[ + Soit $(a, b) in NN^2$. Par la propriété précédente on a $a sect b in {a, b}$, + donc $a sect b = a$ ou $a sect b = b$, ce qui entraîne $a subset b$ ou $b subset a$. +] + +#definition[ + On dit qu'un ensemble $E$ est fini si, et seulement si il existe un entier + $n in NN$ et une bijection de $n$ dans $E$. Sinon, il est dit infini. +] + +#proposition[ + Un tel entier, s'il existe est unique et est appelé cardinal de $E$, et + noté $op("Card") E$, $hash E$ ou $|E|$. +] + +#proposition[ + Toute partie non vide de $NN$ possède un minimum. +] + +#theorem[Schéma de théorème de récurrence][ + Soit $P(n)$ un prédicat. + + Si + $ P(0) quad and quad forall n in NN quad P(n) => P(n+1) $ + alors + $ forall n in NN quad P(n). $ +] + +#proof[ + Soit $P(n)$ un prédicat, et supposons + $ P(0) quad and quad forall n in NN quad P(n) => P(n+1). $ + + Supposons par l'absurde $exists n in NN space not P(n)$. + + Ainsi $A = {n in NN | not P(n)}$ est non vide, donc il est minoré. + Il possède donc un minimum $n_0 in A subset NN$. + + Comme $P(0)$, on a $n_0 != 0$ donc $n_0 - 1 in NN$, et $n_0-1 in.not A$ + car $n_0$ est le minimum de $A$, donc $P(n_0 -1)$. Ainsi par hypothèse + $P(n_0)$, donc $n_0 in.not A$, ce qui est absurde. +] + +#definition[Addition][ + On définit l'application suivante~: + $ +: NN^2 -> NN $ + telle que + $ forall (a, b) in NN² quad a + 0 = a quad and quad a + s(b) = s(a+b). $ +] + +#remark[ + On a toujours $n + 1 = s(n)$. +] + +#proposition[ + L'addition est associative i.e. $ forall (a, b, c) in NN^3 quad a + (b + c) + = (a + b) + c. $ +] + +#proposition[ + L'addition est commutative i.e. $ forall (a, b) in NN^2 quad a + b = b + a. $ +] + + +#definition[Multiplication][ + On définit l'application suivante~: + $ times : NN^2 -> NN $ telle que + $ forall (a, b) in NN² quad a times 1 = a quad and quad a times (b + 1) + = a times b + a. $ +] + +#proposition[ + La multiplication est associative i.e. $ forall (a, b, c) in NN^3 quad a + times (b times c) = (a times b) times c. $ +] + +#proposition[ + La multiplication est commutative i.e. $ forall (a, b) in NN^2 quad a + times b = b times a. $ +] + +#proposition[ + La multiplication est distributive par rapport à l'addition i.e. + $ forall (a, b, k) in NN quad k(a+b) = k a + k b. $ +] + + += Entiers relatifs et arithmétique + +#definition[ + On dit que deux couples d'entiers naturels $(a, b)$ et $(c, d)$ sont + équidistants si, et seulement si $a + d = b + c$. On notera ici + $(a, b) tilde.op (c, d)$ +] + +#proposition[ + L'équipollence est une relation d'équivalence sur $NN^2$. +] + +#definition[ + On appelle ensemble des entiers relatifs, noté $ZZ$, l'ensemble $NN^2 + slash tilde$. +] + += Nombres rationnels + +== Ensemble $QQ$ + +#definition[ + Soit $(a, b) in ZZ times NN^*$. Le couple $(a, b)$ est appelé fraction de + $a$ sur $b$ et notée $display(a/b)$. +] + +#definition[ + Soient $display(a/b)$ et $display(c/d)$ deux fractions. On note~: + $ a/b + c/d &= (a d+b c)/(b d) \ + a/b times c/d &= (a c)/(b d). $ +] + +#definition[ + On définit sur l'ensemble des fractions $E = ZZ times NN^*$ la relation + définie par $ a/b tilde.op c/d <=> a d = b c. $ + On dit alors que ces deux fractions sont proportionnelles. On appelle + ensemble des nombres rationnels, noté $QQ$, l'ensemble $E slash tilde$. +] + +#proposition[ + L'application $ pi : E &-> QQ \ a/b & |-> op("cl")_tilde (a/b) $ préserve + les opérations $+$ et $times$, c'est-à-dire pour toutes fractions + $display(a/b)$ et $display(c/d)$, on a $ pi(a/b + c/d) = pi(a/b) + pi(c/d) $ +] + +#remark[ + On l'appelle projection canonique sur $QQ$. +] + += Nombres réels et fondements de l'analyse + +Voici la construction la plus délicate... + += Nombres complexes + +#definition[Ensemble des nombres complexes][ + On appelle ensemble des nombres complexes l'ensemble $RR^2$, noté $CC$, + muni des lois $+$ et $times$ définies par + + $ + + : CC^2 & -> CC \ + (a, b), (c, d) & mapsto (a + c, b + d) + $ + et + $ + times : CC^2 & -> CC \ + (a, b), (c, d) & mapsto (a c - b d, a d + b c) + $ +] + +#notation[ + Le couple $(a, b)$ se note alors $a + i b$. Le réel $x$ est identifié à + $(x, 0)$. +]