Mathlib Map

Theorems · Definition · category theory

BddLat.of

(α : Type u_1) → [inst : Lattice α] → [BoundedOrder α] → BddLat

Construct a bundled BddLat from Lattice + BoundedOrder.

Defined in
Mathlib.Order.Category.BddLat
Cited by
4 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
LatticeBoundedOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BddLat.dual · cited by 8BddLat.dualBddLat.ofHom · cited by 3BddLat.ofHomBddDistLat.toBddLat · cited by 1BddDistLat.toBddLatBddLat.coe_of · cited by 0BddLat.coe_ofBddLat.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 0latToBddLatLattice · cited by 916LatticeBoundedOrder · cited by 270BoundedOrderBddLat · cited by 27BddLatBddLat.ofCITED BYCITES

Cites3

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

Cited by8

Results whose statement or proof uses this declaration.