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

Andreas





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