Commit 2021-03-27 03:05 ec26d96a

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.