Theorems · Definition · order theory

LatticeHom.withBot

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

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

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

4 results in Mathlib

Foundations

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

Assumes

LatticeLattice