Re: [isabelle] extending well-founded partial orders to total well-founded orders
Yes, you're right, this is exactly the last lemma in Zorn. I must have
missed it when I last looked at that theory.
It uses the existence of a well-ordering on any set. I don't know
whether that has been proven in Isabelle before. Andrei might have done
so in his Cardinals development; he might tell you more.
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and
This archive was generated by a fusion of
Pipermail (Mailman edition) and