Last statement of the non-well-founded induction theorem.

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