nat.succ as an embedding

Stream: Is there code for X?

[Yakov Pechersky]

Do we have nat.succ as an embedding? Probably as an order embedding, which I can then forget to just an embedding.

[Eric Rodriguez]

I'm surprised that there isn't any for docs#order.succ, actually... cc @Yaël Dillies

[Yaël Dillies]

That's very easy to write, actually.

[Eric Rodriguez]

all we need is a no_top_order, right?

[Kyle Miller]

I'm sort of surprised docs#function.injective.to_embedding doesn't exist.

Anyway, there's at least function.embedding.mk _ nat.succ_injective for now.

[Yaël Dillies]

import order.succ_pred.basic

namespace order
variables {α : Type*} [partial_order α] [succ_order α] [no_max_order α]

/-- `order.succ` as an order embedding. -/
@[simps] def succ_embedding : α ↪o α := order_embedding.of_map_le_iff succ $ λ _ _, succ_le_succ_iff

end order

[Yaël Dillies]

Could hardly do shorter! :stuck_out_tongue:

[Yaël Dillies]

We also need antisymmetry because succ is potentially misbehaved on indistinguishable points.

[Yakov Pechersky]

We have addition as an order embedding somewhere, so one could use that. Don't remember what it's called at the moment.

[Eric Wieser]

docs#add_right_embedding

[Yakov Pechersky]

That's the plain embedding. We don't have that as the order one?

[Violeta Hernández]

There's already sections in the order/succ_pred/basic.lean file that have these exact assumptions as variables

[Violeta Hernández]

So this definition should be PR'd at the end of said section

[Violeta Hernández]

Also, the analogous embedding for pred should be PR'd too