Structures · Order

FrameHomClass

FrameHomClass F α β states that F is a type of frame morphisms. They preserve ⊓ and ⨆. You should extend this class when you extend FrameHom.

Defined in

Mathlib.Order.Hom.CompleteLattice

Shape

3 explicit arguments · adds map_sSup