coe_of

Mathlib.Order.Category.BddDistLat

URI: https://scilib.ai/kg/mathlib#BddDistLat.coe_of

English

The underlying type of the bundled object BddDistLat.of α is precisely α.

Русский

Базовый тип упакованного объекта BddDistLat.of α равен α.

LaTeX

$$$\\uparrow(\\text{of } \\alpha) = \\alpha$$$

Lean4

theorem coe_of (α : Type*) [DistribLattice α] [BoundedOrder α] : ↥(of α) = α :=
  rfl

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

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

Разделы

Аффилиация

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