Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
We do have an entry lexicographic order; does it meet your needs? I guess a remark could be put in about the case where the orders involved are well-ordered. Thanks for the suggestion!
I think that for nonempty , the product under the lexicographic order is well-founded if and only if all the are well-founded. This is because each embeds as a suborder of , and a suborder of a well-founded order is also well-founded. So you need to be able to do induction over all the in order to do induction over .
Thanks for pointing out the error under the Examples section; I think it’s fixed now.
1 to 6 of 6