From b7858bd1b5faab9edf00716321a8176981bb6c17 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Sat, 30 Jan 2016 18:01:12 +0100 Subject: Last statement of the non-well-founded induction theorem. --- notes-mitro206.tex | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'notes-mitro206.tex') 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}$ -- cgit v1.2.3