Existenz von Fixpunkten

Fixpunkt von f : : C→C mathend000# ist x : : C mathend000# mit fx = x mathend000#.

Existenz? Eindeutigkeit? Konstruktion?

Satz: Wenn C mathend000# pointed CPO und f mathend000# stetig,
dann besitzt f mathend000# genau einen kleinsten Fixpunkt.

• CPO = mathend000# complete partial order = mathend000# vollständige Halbordnung
• complete = mathend000# jede monotone Folge besitzt Supremum (= mathend000# kleinste obere Schranke)
• pointed: C mathend000# hat kleinstes Element $\bot$ mathend000#
• stetig: x≤y⇒f (x)≤f (y) mathend000# und für monotone Folgen [x₀, x₁,…] mathend000# gilt: f (sup[x₀, x₁,…]) = sup[f (x₀), f (x₁),…] mathend000#

Dann fix(f )= sup[$\bot$, f ($\bot$), f²($\bot$),…] mathend000#