Theorems · Definition · order theory

SupBotHom.dual

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] → [inst_1 : Bot α] → [inst_2 : Max β] → [inst_3 : Bot β] → SupBotHom α β ≃ InfTopHom αᵒᵈ βᵒᵈ

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

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

5 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

MaxBotMaxBot