Forgetful order_embeddings between lattices of substructures

Stream: general

[Junyan Xu]

Which function.injective.something_ordered do you have in mind? The general setting I have in mind is: if A and B are equipped with orders pulled back from C via injective maps f : A ↪ C and g : B ↪ C, and if h : A → B forms a commuting triangle with f and g, then h is an order_embedding.
(edited title to avoid confusion)