Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:tarski_s_fixpoint_theorem [2008/05/07 22:50]
giuliano
sav08:tarski_s_fixpoint_theorem [2009/03/26 10:36] (current)
vkuncak
Line 40: Line 40:
 **Lemma:** The value $a_*$ is a prefix point. **Lemma:** The value $a_*$ is a prefix point.
  
-Observation:​ $a_*$ need not be a fixpoint.+Observation:​ $a_*$ need not be a fixpoint ​(example in exercises, e.g. on lattice [0,1] of real numbers).
  
 **Definition:​** A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have **Definition:​** A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have
 
sav08/tarski_s_fixpoint_theorem.txt · Last modified: 2009/03/26 10:36 by vkuncak
 
© EPFL 2018 - Legal notice