An increasing function is injective

the induced order on a subtype is an embedding under the natural inclusion.

An order embedding is also an order embedding between dual orders.

If f is injective, then it is an order embedding from the preimage order of s to s.

It suffices to prove f is monotone between strict orders to show it is an order embedding.

The inclusion map fin n → ℕ is an order embedding.

The inclusion map fin m → fin n is an order embedding.

An order isomorphism is an equivalence that is also an order embedding.

Any equivalence lifts to an order isomorphism between s and its preimage.

A subset p : set α embeds into α

subrel r p is the inherited relation on a subset.

Restrict the codomain of an order embedding