summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--notes-mitro206.tex13
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}$