Theorems · Definition · order theory

BoundedLatticeHom.dual

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] →
      [inst_1 : BoundedOrder α] →
        [inst_2 : Lattice β] → [inst_3 : BoundedOrder β] → BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ

Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual bounded lattices.

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

11 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

LatticeBoundedOrderLatticeBoundedOrder