Theorems · Definition · order theory

InfHom.dual

{α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : Min β] → InfHom α β ≃ SupHom αᵒᵈ βᵒᵈ

Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

6 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

MinMin