Theorems · Definition · order theory

LatticeHom.withTopWithBot

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

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

Defined in: Mathlib.Order.Hom.WithTopBot
Cited by: 4 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext, Quot.sound
Assumes: Lattice Lattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

WithTopstatement · cited by 3,754
WithBotstatement · cited by 1,498
Latticestatement and proof · cited by 916
LatticeHomstatement and proof · cited by 192
BoundedLatticeHomstatement · cited by 185
LatticeHom.withBotproof · cited by 4
LatticeHom.withTopproof · cited by 4

Cited by5

Results whose statement or proof uses this declaration.

LatticeHom.withTopWithBot_applystatement · cited by 0
LatticeHom.withTopWithBot_compstatement · cited by 0
LatticeHom.withTopWithBot_idstatement and proof · cited by 0
LatticeHom.coe_withTopWithBotstatement · cited by 0
latToBddLatproof · cited by 0