Mathlib Map

Theorems · Definition · order theory

LatticeHom.toSupHom

{α : Type u_6} → {β : Type u_7} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → SupHom α β
Defined in
Mathlib.Order.Hom.Lattice
Cited by
31 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
LatticeLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LatticeHom.comp · cited by 27LatticeHom.compLatticeHom.withBot · cited by 4LatticeHom.withBotLatticeHom.withTop · cited by 4LatticeHom.withTopLatticeHom.map_inf' · cited by 4LatticeHom.map_inf'LatticeHom.withBot' · cited by 2LatticeHom.withBot'LatticeHom.withTop' · cited by 2LatticeHom.withTop'LatticeHom.copy · cited by 2LatticeHom.copyLatticeHom.toInfHom · cited by 2LatticeHom.toInfHomHeytingHom.mk.inj · cited by 1mk.injHeytingHom.mk.noConfusion · cited by 1mk.noConfusionBoundedLatticeHom.toBoundedOrderHom · cited by 1BoundedLatticeHom.toBound…BoundedLatticeHom.toInfTopHom · cited by 1BoundedLatticeHom.toInfTo…BoundedLatticeHom.toSupBotHom · cited by 1BoundedLatticeHom.toSupBo…BiheytingHom.mk.inj · cited by 1mk.injBiheytingHom.mk.noConfusion · cited by 1mk.noConfusionLattice · cited by 916LatticeLatticeHom · cited by 192LatticeHomSupHom · cited by 68SupHomLatticeHom.toSupHomCITED BYCITES

Cites3

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

  • Latticestatement and proof · cited by 916
  • LatticeHomstatement and proof · cited by 192
  • SupHomstatement · cited by 68

Cited by61

Results whose statement or proof uses this declaration.