Email Gateway (Aug 19 2022 at 14:41): Email Gateway (Aug 19 2022 at 14:41):From: John Wickerson <johnwickerson@cantab.net>
Dear all,
I'd like to use the following in my proof:
lemma johns_lemma:
"mono f ⟹ lfp f = (⋃k. (f ^^ k) {})"
I think it's a pretty bog-standard theorem about least fixed points over complete lattices. But I can't find it in the library or the AFP. Does anybody know how I can obtain it?
Best wishes,
John
Email Gateway (Aug 19 2022 at 14:41):From: Brian Huffman <huffman.brian.c@gmail.com>
This theorem needs a stronger assumption, namely that the function f
be continuous, i.e. it preserves least upper bounds (at the very
least, it must preserve lubs of countable chains).
On a general complete lattice, a monotone function may need to be
iterated transfinitely many times before a fixed point is reached.
Email Gateway (Aug 19 2022 at 14:41):From: David Cock <davec@cse.unsw.edu.au>
John,
The lemma you want is continuous_lfp in Library/Continuity.thy.
Dave
Email Gateway (Aug 19 2022 at 14:41):From: Johannes Hölzl <hoelzl@in.tum.de>
Just as a small note: Library/Continuity.thy will be
Library/Order_Continuity.thy in the next Isabelle release. Continuity is
often associated with a topology.
Last updated: Apr 24 2024 at 20:16 UTC