From 2985de4836242f9706d4da27eaf56f7a5bc93914 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 30 Jan 2016 17:39:35 +0100
Subject: Second proof (using ordinals) of the lemma.

---
 notes-mitro206.tex | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'notes-mitro206.tex')

diff --git a/notes-mitro206.tex b/notes-mitro206.tex
index 01790ef..397cc5e 100644
--- a/notes-mitro206.tex
+++ b/notes-mitro206.tex
@@ -1296,6 +1296,29 @@ donc bien trouvé une fonction partielle $f := U(\varnothing)$ telle
 que $\Psi(f) \subseteq f$ (même $\Psi(f) = f$).
 \end{proof}
 
+\begin{proof}[Seconde démonstration]
+On utilise la notion d'ordinaux.  On pose $f_0 = \varnothing$, et par
+induction sur l'ordinal $\alpha$ on définit $f_{\alpha+1} =
+\Psi(f_\alpha)$ et si $\delta$ est un ordinal limite alors $f_\delta =
+\bigcup_{\gamma<\delta} f_\gamma$.  On montre simultanément par
+induction sur $\alpha$ que $f_\alpha$ est bien définie, est une
+fonction partielle, et, grâce à la croissance de $\Psi$, prolonge
+$f_\beta$ pour chaque $\beta<\alpha$ (c'est ce dernier point qui
+permet de conclure que $\bigcup_{\gamma<\delta} f_\gamma$ est une
+fonction partielle lorsque $\delta$ est un ordinal limite : la réunion
+d'une famille totalement ordonnée pour l'inclusion de fonctions
+partielles est encore une fonction partielle).  Les inclusions
+$f_\beta \subseteq f_\alpha$ pour $\beta<\alpha$ ne peuvent pas être
+toutes strictes sans quoi on aurait une surjection d'un ensemble sur
+la classe des ordinaux.  Il existe donc $\tau$ tel que $f_{\tau+1} =
+f_\tau$, c'est-à-dire $\Psi(f_\tau) = f_\tau$.  D'autre part, si
+$\Psi(h) = h$, alors par induction sur $\alpha$ on montre $f_\alpha
+\subseteq h$ pour chaque $\alpha$ (l'étape successeur étant que si
+$f_\alpha \subseteq h$ alors $f_{\alpha+1} = \Psi(f_\alpha) \subseteq
+\Psi(h) = h$), donc en particulier $f_\tau \subseteq h$, et $f_\tau$
+est bien le plus petit $f$ tel que $\Psi(f) = f$.
+\end{proof}
+
 
 
 \subsection{Écrasement transitif}
-- 
cgit v1.2.3

