Structures · Order

CompleteSemilatticeSup

Note that we rarely use CompleteSemilatticeSup (in fact, any such object is always a CompleteLattice, so it's usually best to start there). Nevertheless it is sometimes a useful intermediate step in constructions.

Defined in

Mathlib.Order.CompleteLattice.Defs

Shape

One type argument · adds isLUB_sSup