author | huffman |
Sun, 07 Feb 2010 10:15:15 -0800 | |
changeset 35055 | f0ecf952b864 |
parent 35012 | c3e3ac3ca091 |
child 35056 | d97b5c3af6d5 |
src/HOLCF/Fix.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOLCF/Fix.thy Sat Feb 06 16:32:34 2010 +0100 +++ b/src/HOLCF/Fix.thy Sun Feb 07 10:15:15 2010 -0800 @@ -73,6 +73,10 @@ apply simp done +lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f" + unfolding fix_def2 + using chain_iterate by (rule is_ub_thelub) + text {* Kleene's fixed point theorems for continuous functions in pointed omega cpo's