Теорема Кнастера-Тарського-Кліні

Нехай D - $\omega$-область, $\varphi: D \to D$ - неперервне відображення задане на цій області. Тоді існує найменша нерухома точка $\varphi$, яка позначається $lfp\ \varphi$, для якої справедлива формула:

$lfp\ \varphi = \bigsqcup_{i \in \omega} \varphi^{(i)} ( \perp )$,

де $\varphi^{(0)}(\perp ) = \perp\ \varphi^{(i+1)}(\perp ) = \varphi (\varphi^{(i)} (\perp ) ),\, i \in \omega$

Доведення

Доведення складається з трьох частин:

• Доведення факту, що множина $\{ \varphi^{(i)} (\perp ) \} i \in \omega$ - ланцюг (тому її супремум $\bigsqcup_{i \in \omega} \varphi^{(i)} ( \perp )$ існує ).
• Доведення того, що $\bigsqcup_{i \in \omega} \varphi^{(i)} ( \perp )$ є нерухомою точкою $\varphi$.
• Доведення, що $\bigsqcup_{i \in \omega} \varphi^{(i)} ( \perp )$ є найменшою з нерухомих точок $\varphi$.