Mathlib Map

Theorems · Definition · category theory

BddLat.toLat

BddLat → Lat

The underlying lattice of a bounded lattice.

Defined in
Mathlib.Order.Category.BddLat
Cited by
24 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BddLat.dual · cited by 8BddLat.dualBddLat.Hom.hom · cited by 3Hom.homBddLat.dualEquiv · cited by 2BddLat.dualEquivBddLat.Hom.ext · cited by 2Hom.extBddLat.Hom.hom' · cited by 2Hom.hom'BddLat.Iso.mk · cited by 2Iso.mkBddLat.ext · cited by 1BddLat.extBddLat.hom_ext · cited by 1BddLat.hom_extlatToBddLatForgetAdjunction · cited by 0latToBddLatForgetAdjuncti…BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat · cited by 0BddDistLat.forget_bddLat_…BddLat.Hom.ext_iff · cited by 0Hom.ext_iffBddLat.coe_forget_to_bddOrd · cited by 0BddLat.coe_forget_to_bddO…BddLat.coe_forget_to_lat · cited by 0BddLat.coe_forget_to_latBddLat.coe_forget_to_semilatInf · cited by 0BddLat.coe_forget_to_semi…BddLat.coe_forget_to_semilatSup · cited by 0BddLat.coe_forget_to_semi…Lat · cited by 43LatBddLat · cited by 27BddLatBddLat.toLatCITED BYCITES

Cites2

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

  • Latstatement · cited by 43
  • BddLatstatement and proof · cited by 27

Cited by35

Results whose statement or proof uses this declaration.