summaryrefslogtreecommitdiffstats
path: root/notes-mitro206.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2016-01-30 17:01:12 (GMT)
committerDavid A. Madore <david+git@madore.org>2016-01-30 17:01:12 (GMT)
commitb7858bd1b5faab9edf00716321a8176981bb6c17 (patch)
tree012648258dccc7e0d0c85be0c0a57ba0aeea2a61 /notes-mitro206.tex
parent2985de4836242f9706d4da27eaf56f7a5bc93914 (diff)
downloadmitro206-b7858bd1b5faab9edf00716321a8176981bb6c17.zip
mitro206-b7858bd1b5faab9edf00716321a8176981bb6c17.tar.gz
mitro206-b7858bd1b5faab9edf00716321a8176981bb6c17.tar.bz2
Last statement of the non-well-founded induction theorem.
Diffstat (limited to 'notes-mitro206.tex')
-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}$