Theorems · Definition · order theory

CompleteLatticeHom.dual

{α : Type u_2} →
  {β : Type u_3} →
    [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β ≃ CompleteLatticeHom αᵒᵈ βᵒᵈ

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

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

8 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

CompleteLatticeCompleteLattice