# Commit 2021-03-27 03:05 ec26d96a

View on Github →feat(order/lattice): add complete_semilattice_Sup/Inf (#6797)
This adds `complete_semilattice_Sup`

and `complete_semilattice_Inf`

above `complete_lattice`

.
This has not much effect, as in fact either implies `complete_lattice`

. However it's useful at times to have these, when you can naturally define just one half of the structure at a time (e.g. the subobject lattice in a general category, where for `Sup`

we need coproducts and images, while for the `Inf`

we need wide pullbacks).
There are many places in mathlib that currently use `complete_lattice_of_Inf`

. It might be slightly nicer to instead construct a `complete_semilattice_Inf`

, and then use the new `complete_lattice_of_complete_semilattice_Inf`

, but I haven't done that here.