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 Li involved are well-ordered. Thanks for the suggestion!
I think that for nonempty Si, the product ∏iSi under the lexicographic order is well-founded if and only if all the Si are well-founded. This is because each Si embeds as a suborder of ∏iSi, and a suborder of a well-founded order is also well-founded. So you need to be able to do induction over all the Si in order to do induction over ∏iSi.
Thanks for pointing out the error under the Examples section; I think it’s fixed now.
1 to 6 of 6