booleanAlgebra

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.booleanAlgebra

English

Finite subsets of α form a Boolean algebra (when α has decidable equality).

Русский

Конечные подмножества α образуют булеву алгебру (при decidable equality α).

LaTeX

$$$\text{BooleanAlgebra}(\mathrm{Finset}(\alpha))$ with decidable equality on α$$

Lean4

instance booleanAlgebra [DecidableEq α] : BooleanAlgebra (Finset α) :=
  GeneralizedBooleanAlgebra.toBooleanAlgebra

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

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

Разделы

Аффилиация

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