add_monoid_hom and ordered_embedding

Stream: maths

[Apurva Nakade]

I have a map f : X ->+ Y and I want to say that f is also an order_embedding.
What's the proper way to say this? Is there some bundled variant of add_monoid_hom_order_embedding?

[Apurva Nakade]

Also, there seems to be two different naming conventions for ordered stuff: ordered_... and order_...
Is this on purpose?

[Eric Wieser]

I think you have to pick between using an embedding and map_zero / map_add assumptions, or an add_monoid_hom and monotone / injective assumptions

[Eric Wieser]

I think you have to pick between using an embedding and map_zero / map_add assumptions, or an add_monoid_hom and monotone / injective assumptions

[Eric Wieser]

I think you have to pick between using an embedding and map_zero / map_add assumptions, or an add_monoid_hom and monotone / injective assumptions

[Eric Wieser]

I think usually we choose the latter

[Apurva Nakade]

Sounds good, thanks!

[Eric Wieser]

As an example docs#submonoid.subtype meets all those conditions

[Eric Wieser]

With injectivity proved as docs#set_like.coe_injective and monotonicity proved as docs#set_like.coe_mono