Theorems · Definition · order theory

LatticeHom.withTop

{α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → LatticeHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of a LatticeHom.

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

4 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

LatticeLattice