diff options
| -rw-r--r-- | notes-mitro206.tex | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/notes-mitro206.tex b/notes-mitro206.tex index 397cc5e..e108570 100644 --- a/notes-mitro206.tex +++ b/notes-mitro206.tex @@ -1210,10 +1210,19 @@ la fonction partielle $x \mapsto \Phi(x, f|_{\outnb(x)})$. Remarquons que si $f$ prolonge $g$ dans $\mathscr{D}$ alors $\Psi(f)$ prolonge $\Psi(g)$ (c'est une traduction de la cohérence supposée sur $\Phi$). Le lemme suivant (appliqué à $X=G$, les autres notations -étant inchangées) permet de conclure. +étant inchangées) permet de conclure à l'existence de $f$. + +Pour ce qui est de la dernière affirmation, on procède par induction +bien-fondée sur la partie bien-fondée de $G$ : si $f|_{\outnb(x)}$ est +totale, i.e., si $f$ est définie sur chaque voisin sortant de $x$, +alors l'hypothèse faite sur $\Phi$ assure que $f(x)$ est définie, et +l'induction bien-fondée ((\ddag) de \ref{well-founded-induction} +appliqué à l'intersection $P$ de la partie bien-fondée de $G$ et de +l'ensemble de définition de $f$) montre alors que $f$ est définie +partout sur la partie bien-fondée de $G$. \end{proof} -La démonstration du théorème repose entièrement sur le lemme suivant, +La démonstration du théorème repose crucialement sur le lemme suivant, dont on va donner deux démonstrations : \begin{lem} Soient $X$ et $Z$ deux ensembles quelconques : notons $\mathscr{D}$ |