Conditionally complete semilattice

Stream: Is there code for X?

[Aaron Liu]

Any conditionally complete semilattice is a conditionally complete lattice, but we also have docs#CompleteSemilatticeSup and docs#CompleteSemilatticeInf.

[Yaël Dillies]

What is your question?

[Aaron Liu]

Do we not have conditionally complete semilattices in mathlib, or am I not looking hard enough? Should we have them?

[Yaël Dillies]

Probably not. As you said, they are just conditionally complete lattices with extra steps. What we should instead have is a constructor for docs#ConditionallyCompleteLattice that only asks for sSup. docs#CompleteSemilatticeSup and docs#CompleteSemilatticeInf could be removed, in fact, according to that same argument.

[Yaël Dillies]

I believe the only reason CompleteSemilatticeSup/CompleteSemilatticeInf are still around is precisely to make that sSup-only constructor for docs#CompleteLattice nice to use

[Bhavik Mehta]

See also the discussion here #mathlib4 > Custom structure constructors with `where` @ 💬, which this design is also an instance of