Theorems · Definition · category theory
BddDistLat.of
(α : Type u_1) → [inst : DistribLattice α] → [BoundedOrder α] → BddDistLat
Construct a bundled BddDistLat from a BoundedOrder DistribLattice.
- Defined in
- Mathlib.Order.Category.BddDistLat
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- DistribLatticeBoundedOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BoundedOrderstatement and proof · cited by 270
- DistribLatticestatement and proof · cited by 150
- BddDistLatstatement · cited by 39
Cited by13
Results whose statement or proof uses this declaration.
- BddDistLat.ofHomstatement · cited by 9
- BddDistLat.dualproof · cited by 6
- BoolAlg.toBddDistLatproof · cited by 1
- BddDistLat.ofHom_applystatement · cited by 0
- BddDistLat.ofHom_compstatement · cited by 0
- BddDistLat.ofHom_homstatement · cited by 0
- BddDistLat.ofHom_idstatement · cited by 0
- BddDistLat.Iso.mk_homstatement · cited by 0
- BddDistLat.Iso.mk_invstatement · cited by 0
- BddDistLat.dual_mapstatement · cited by 0
- BddDistLat.hom_ofHomstatement · cited by 0
- HeytAlg.hasForgetToLat_forget₂_mapstatement · cited by 0