coe_of

Mathlib.Order.Category.FinBoolAlg

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

English

For a Boolean algebra α with finite basis, the carrier of FinBoolAlg.of α is α.

Русский

Для булевой алгебры α с конечной базой каркас FinBoolAlg.of α равен α.

LaTeX

$$$ (\\mathrm{FinBoolAlg}.of\\; \\alpha).\\mathrm{carrier} = \\alpha. $$$

Lean4

theorem coe_of (α : Type*) [BooleanAlgebra α] [Fintype α] : ↥(of α) = α :=
  rfl

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

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

Разделы

Аффилиация

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