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.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
