Twierdzenie Knastera-Tarskiego o punkcie stałym

Twierdzenie Knastera-Tarskiego o punkcie stałym - twierdzenie mówiące, że jeżeli P jest kratą zupełną oraz funkcja $f\colon P \to P$ jest monotoniczna, to ma ona punkt stały, co więcej zbiór wszystkich punktów stałych jest również kratą zupełną. Twierdzenie udowodnione najpierw przez Bronisława Knastera dla zbiorów potęgowych, później podane w pełnej ogólności przez Alfreda Tarskiego. Ma ono szereg ważnych zastosowań w semantyce języków programowania.

Twierdzenie

Dla kraty zupełnej $( P, \le )$ oraz funkcji monotonicznej $f\colon P \to P$ określonej na tej kracie, istnieje najmniejszy punkt stały funkcji $f$, tzn.

$\exists_{x \in P}\; f(x) = x$

oraz

$\forall_{y \in P}\; f(y) = y \implies x \le y$

Należy podkreślić, że funkcja $f$ musi być funkcją monotoniczną na porządku zupełnym, a nie w znaczeniu analizy matematycznej. W szczególności twierdzenie nie jest prawdziwe dla funkcji antymonotonicznych (np. krata $([0; 1], \le)$ oraz indykator zbioru $[0; 1/2]$).