sum.lex and prod.lex as rel_embeddings

Stream: Is there code for X?

[Violeta Hernández]

Specifically, the obvious embeddings r ↪r sum.lex r s, s ↪r sum.lex r s, and the embeddings r ↪r prod.lex r s and s ↪r prod.lex r s given an element in the other type

[Violeta Hernández]

Would also be nice to have things like s ↪r t → sum.lex r s ↪r sum.lex r t

[Violeta Hernández]

We could lift a lot of these into initial segments, and use them to golf the basic ordinal API

[Eric Wieser]

Do we have these for the specialization to ≤?

[Violeta Hernández]

I doubt it, we don't have any special way to write sum.lex (≤) (≤)

[Violeta Hernández]

As far as I'm aware

[Yaël Dillies]

docs#sum.lex.preorder

[Yaël Dillies]

The special way to write sum.lex (≤) (≤) is (≤).

[Violeta Hernández]

Well, there's a few lemmas about order isomorphisms but I can't see anything about relation embeddings

[Eric Wieser]

Yaël Dillies said:

The special way to write sum.lex (≤) (≤) is (≤).

No it's not, it's (≤) on to_lex

[Eric Wieser]

docs#sum.lex.to_lex_mono is the statement I'm thinking of, I guess we don't have the bundling. Maybe we have the bundled sum.inl for docs#sum.preorder

[Eric Wieser]

Again no bundling, but we have src#sum.lex.inl_mono

[Violeta Hernández]

I guess I could prove the bundled versions on arbitrary relations and then use those to golf these theorems

[Eric Wieser]

src#sum.lex.to_lex_mono isn't exactly in need of further golfing

[Violeta Hernández]

Wait a second

[Violeta Hernández]

That doesn't seem right

[Violeta Hernández]

docs#order_iso.sum_comm

[Violeta Hernández]

Oh wait nevermind, that's not the same relation

[Violeta Hernández]

#15355