Composition of Order Embeddings

Stream: Is there code for X?

[Eric Paul]

Do we have a theorem that says that the composition of order embeddings is an order embedding?
I expected there to be one but I can't seem to find it.

Something of this form:

comp : α ↪o β → β ↪o γ → α ↪o γ

[Yaël Dillies]

docs#OrderEmbedding.comp is missing

[Eric Paul]

I'll make a PR for it then.
(Should I?)

Thanks for confirming it isn't there.

[Eric Paul]

Ah we already have the composition of RelEmbedding and OrderEmbedding is just an abbreviation for it.
So this does already exist