Theorems · Inductive type · order theory

SupHomClass

(F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Max α] → [Max β] → [FunLike F α β] → Prop

SupHomClass F α β states that F is a type of ⊔-preserving morphisms. You should extend this class when you extend SupHom.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

11 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

MaxMaxFunLike