Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
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