Commit 2021-03-27 03:05 ec26d96aView on Github →
feat(order/lattice): add complete_semilattice_Sup/Inf (#6797)
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.
added theorem ennreal.supr_zero_eq_zero
modified theorem Inf_le
modified theorem Sup_le
modified theorem le_Inf
modified theorem le_Sup