Theorems · Inductive type · order theory

InfHomClass

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

InfHomClass F α β states that F is a type of ⊓-preserving morphisms. You should extend this class when you extend InfHom.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

10 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

MinMinFunLike