From 91f5489f36797c6cf4ab76e1f9dd07e601b2d390 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 18 Dec 2015 17:10:14 +0100
Subject: Definition by non-well-founded induction.

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

(limited to 'notes-mitro206.tex')

diff --git a/notes-mitro206.tex b/notes-mitro206.tex
index 20f6ee3..ac9033a 100644
--- a/notes-mitro206.tex
+++ b/notes-mitro206.tex
@@ -1134,6 +1134,73 @@ toute partie aval-inductive de $G$ est, en particulier, dans la partie
 bien-fondée de $G$.
 \end{proof}
 
+\thingy Pour pouvoir énoncer le théorème suivant, on aura besoin de
+faire les rappels, définitions et remarques suivants.  Une
+\textbf{fonction partielle} $A \dasharrow Z$, où $A$ est un ensemble
+quelconque, n'est rien d'autre qu'une fonction définie $D \to Z$ sur
+une partie $D\subseteq A$ de $Z$ (appelée \textbf{ensemble de
+  définition} de la partie).  Si $f,g\colon A \dasharrow Z$ sont deux
+fonctions partielles, on dit que $f$ \textbf{prolonge} $g$ et on note
+$f \supseteq g$ ou $g\subseteq f$, lorsque l'ensemble de définition
+$D_f$ de $f$ contient celui $D_g$ de $g$ et que $f$ et $g$ coïncident
+sur $D_f$ (ceci signifie bien que $f \supseteq g$ en tant qu'ensembles
+si on identifie une fonction avec son graphe).  Il s'agit bien sûr là
+d'un ordre partiel (sur l'ensemble des fonctions partielles $A
+\dasharrow Z$).
+
+Enfin, si $\Phi$ est une fonction partielle elle-même définie sur
+l'ensemble des fonctions partielles $A \dasharrow Z$ (cet ensemble est
+$\bigcup_{D\subseteq A} Z^D$, si on veut), on dit que $\Phi$ est
+\textbf{cohérente} lorsque $\Phi(f) = \Phi(g)$ à chaque fois que $f$
+prolonge $g$ et que $\Phi(g)$ est définie (autrement dit, une fois que
+$\Phi$ est définie sur une fonction partielle $g$, elle est définie
+sur tout prolongement de $g$ et y prend la même valeur que sur $g$ ;
+intuitivement, il faut s'imaginer que si $g$ apporte assez
+d'information pour décider la valeur de $\Phi(g)$, toute information
+supplémentaire reste cohérente avec cette valeur).
+
+\begin{thm}\label{non-well-founded-definition}
+Soit $G$ un graphe orienté et $Z$ un ensemble quelconque.
+Notons $\outnb(x) = \{y : (x,y) \in E\}$ l'ensemble des
+voisins sortants d'un sommet $x$ de $G$ (i.e., des $y$ atteints par une
+arête de source $x$).
+
+Appelons $\mathscr{F}$ l'ensemble des couples $(x,f)$ où $x\in G$ et
+$f$ une fonction \emph{partielle} de l'ensemble des voisins sortants
+de $x$ vers $Z$ (autrement dit, $\mathscr{F}$ est $\bigcup_{x \in G}
+\bigcup_{D \subseteq \outnb(x)} \big(\{x\}\times Z^D\big)$).  Soit
+enfin $\Phi\colon \mathscr{F} \dasharrow Z$ une fonction cohérente en
+la deuxième variable, c'est-à-dire telle que $\Phi(x,f) = \Phi(x,g)$
+dès que $f \supseteq g$.  Alors il existe une plus petite (au sens du
+prolongement) fonction partielle $f\colon G \dasharrow Z$ telle que
+pour tout $x \in G$ on ait
+\[
+f(x) = \Phi(x,\, f|_{\outnb(x)})
+\]
+(au sens où chacun des deux membres est défini ssi l'autre l'est, et
+dans ce cas ils ont la même valeur).
+
+Si $\Phi(x,g)$ est défini à chaque fois que $g$ est totale, alors la
+fonction $f$ qu'on vient de décrire est définie \emph{au moins} sur la
+partie bien-fondée de $G$.
+\end{thm}
+\begin{proof}
+Soit $\Gamma$ le plus petit ensemble de couples $(x,z) \in G \times Z$
+tel que (*) à chaque fois que $x\in G$ et que $g\colon \outnb(x)
+\dasharrow Z$ est inclus dans $\Gamma$ (au sens où $(y,g(y)) \in
+\Gamma$ pour chaque $y$ sur lequel $g$ est défini) on ait $(x,
+\Phi(x,g)) \in \Gamma$.  Ce plus petit ensemble a bien un sens car une
+intersection quelconque de parties de $G\times Z$ vérifiant (*)
+vérifie encore (*) (ceci est vrai puisque la condition (*) est de la
+forme « si certains éléments appartiennent à la partie, alors d'autres
+  éléments appartiennent à la partie »).
+
+Afin de pouvoir définir $f(x)$ comme le $z$ tel que $(x,z) \in \Gamma$
+s'il existe (autrement dit, la fonction de graphe $\Gamma$), il faut
+montrer qu'il y a \emph{au plus un} tel $z$.  \textcolor{red}{...}
+\end{proof}
+
+
 
 \subsection{Écrasement transitif}
 
-- 
cgit v1.2.3