Re: [isabelle] extending well-founded partial orders to total well-founded orders

Dear Christian,

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
Yes, you're right, this is exactly the last lemma in Zorn. I must have missed it when I last looked at that theory.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.