English
From a type α with a distributive lattice, a bounded order, and finite cardinality, one forms a FinBddDistLat with carrier α.
Русский
Из типа α с распределенной решеткой, ограниченным порядком и конечностью образуется FinBddDistLat с носителем α.
LaTeX
$$FinBddDistLat.of α$$
Lean4
/-- Construct a bundled `FinBddDistLat` from a `Fintype` `BoundedOrder` `DistribLattice`. -/
abbrev of (α : Type*) [DistribLattice α] [BoundedOrder α] [Fintype α] : FinBddDistLat where carrier := α