Theorems · Inductive type · order theory

InfTopHom

(α : Type u_6) → (β : Type u_7) → [Min α] → [Min β] → [Top α] → [Top β] → Type (max u_6 u_7)

The type of finitary infimum-preserving homomorphisms from α to β.

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

60 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

MinMinTopTop