Discrete partial order

Stream: mathlib4

[Jad Ghalayini]

Hello! I'm doing some PL formalization which needs to reason about partial orders, and I would like to have the discrete partial order as a base case. I've defined a Lex-like def Disc which equips an arbitrary type with the discrete order; is this the right way to go about it? And would such a thing have a place in mathlib? I've also defined a whole bunch of utilities w.r.t e.g. WithBot (Disc α) but I have no idea if I'm doing it in the correct style rip...

[Yaël Dillies]

Hey Jad! Nice to see you here

[Yaël Dillies]

I think this is a perfectly reasonable approach, although I would suggest a more descriptive name than Disc, eg WithDiscreteOrder. You can look around docs#Topology.WithLower for the general pattern

[Jad Ghalayini]

Makes sense, thanks! What would the path be like for getting this into mathlib? Also, it would be useful to add a PartialOrder instance for Option α which is just the union of the partial order on α and none = none, but I don't want to break anything. Any advice about that?

[Yaël Dillies]

Ask for permission to create a PR in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission, create a branch on the mathlib4 repo, open a PR from it, request my review, wait a month for me to be done with exams :grinning:

[Yaël Dillies]

Jad Ghalayini said:

it would be useful to add a PartialOrder instance for Option α which is just the union of the partial order on α and none = none

We've discussed this before in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Preorder.20on.20Option

[Jad Ghalayini]

Yaël Dillies said:

Ask for permission to create a PR in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission, create a branch on the mathlib4 repo, open a PR from it, request my review, wait a month for me to be done with exams :grinning:

I believe I already have perms, so will do! Thanks again!