Mathlib Map

Theorems · Definition · order theory

Lat.carrier

Lat → Type u_1

The underlying lattices.

Defined in
Mathlib.Order.Category.Lat
Cited by
58 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.

Lat.Hom.hom · cited by 11Hom.homBddLat.dual · cited by 8BddLat.dualLat.dual · cited by 7Lat.dualBddLat.Hom.hom · cited by 3Hom.homBddLat.dualEquiv · cited by 2BddLat.dualEquivLat.dualEquiv · cited by 2Lat.dualEquivBddLat.Hom.ext · cited by 2Hom.extBddLat.Hom.hom' · cited by 2Hom.hom'BddLat.Iso.mk · cited by 2Iso.mkLat.Hom.ext · cited by 2Hom.extLat.Hom.hom' · cited by 2Hom.hom'Lat.Iso.mk · cited by 2Iso.mkBddLat.ext · cited by 1BddLat.extBddLat.hom_ext · cited by 1BddLat.hom_extLat.ext · cited by 1Lat.extLat · cited by 43LatLat.carrierCITED BYCITES

Cites1

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

  • Latstatement and proof · cited by 43

Cited by85

Results whose statement or proof uses this declaration.