of'

Mathlib.Order.Category.FinBddDistLat

URI: https://scilib.ai/kg/mathlib#FinBddDistLat.of'

Lean4

/-- Construct a bundled `FinBddDistLat` from a `Nonempty` `Fintype` `DistribLattice`. -/
abbrev of' (α : Type*) [DistribLattice α] [Fintype α] [Nonempty α] : FinBddDistLat
    where
  carrier := α
  isBoundedOrder := Fintype.toBoundedOrder α

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru