Mathlib Map

Theorems · Definition · category theory

BddLat.ofHom

{X Y : Type u} →
  [inst : Lattice X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : Lattice Y] → [inst_3 : BoundedOrder Y] → BoundedLatticeHom X Y → (BddLat.of X ⟶ BddLat.of Y)

Typecheck a BoundedLatticeHom as a morphism in BddLat.

Defined in
Mathlib.Order.Category.BddLat
Cited by
3 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LatticeBoundedOrderLatticeBoundedOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BddLat.dual · cited by 8BddLat.dualBddLat.Iso.mk · cited by 2Iso.mklatToBddLatForgetAdjunction · cited by 0latToBddLatForgetAdjuncti…BddLat.dual_map · cited by 0BddLat.dual_mapBddLat.Iso.mk_hom · cited by 0Iso.mk_homBddLat.Iso.mk_inv · cited by 0Iso.mk_invlatToBddLat · cited by 0latToBddLatQuiver.Hom · cited by 32603Quiver.HomLattice · cited by 916LatticeBoundedOrder · cited by 270BoundedOrderBoundedLatticeHom · cited by 185BoundedLatticeHomBddLat · cited by 27BddLatCategoryTheory.ConcreteCategory.ofHom · cited by 18ConcreteCategory.ofHomBddLat.of · cited by 4BddLat.ofBddLat.ofHomCITED BYCITES

Cites7

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

Cited by7

Results whose statement or proof uses this declaration.