Zulip Chat Archive
Stream: Is there code for X?
Topic: well-founded linear order on a type
Yury G. Kudryashov (Feb 22 2021 at 21:32):
Do we a theorem that says "every type admits a well-founded linear order"?
Yury G. Kudryashov (Feb 22 2021 at 22:11):
Found docs#cardinal.ord_eq
Yury G. Kudryashov (Feb 22 2021 at 22:13):
And docs#cardinal.well_ordering_rel
Last updated: Dec 20 2023 at 11:08 UTC