complete partial order formalization

Stream: mathlib4

[Jad Ghalayini]

Hello! I'm interested in formalizing complete partial orders, which don't seem to be formalized in Mathlib 3 as far as I can tell. Are you guys taking new files by any chance? It should be a pretty simple formalization since none of the results I'm aiming for are particularly complicated; I'm putting it together in my private formalization and it seems like a good idea to merge it in so new Mathlib releases don't break it.

[Reid Barton]

Is that different from docs#complete_lattice?

[Reid Barton]

Or docs#omega_complete_partial_order?

[Yury G. Kudryashov]

Wikipedia mentions 3 different notions: https://en.wikipedia.org/wiki/Complete_partial_order

[Yury G. Kudryashov]

Which one are you talking about?

[Yury G. Kudryashov]

How will your formalization interact with existing typeclasses?

[Jad Ghalayini]

Welp I didn't even realize it was already formalized, pretty silly. I guess I'll just try porting that, then

[Reid Barton]

Feel free to take over mathlib4#1168 although I got annoyed at a bug in simp breaking many proofs.

[Reid Barton]

Or more precisely, I think it would be better to fix simp first (since I imagine not much of mathlib can be waiting for this module).