instBooleanAlgebra — Mathlib

English

The collection of definable sets over A with parameter α forms a Boolean algebra under the induced operations (sup, inf, com, sdiff, himp, top, bot).

Русский

Множество определяемых множеств над A с параметром α образует булову алгебру при введённых операциях (верх, низ, дополенение, разность, импликация, вершина, ноль).

LaTeX

$$$$ \\text{BooleanAlgebra}(L.DefinableSet A α) $$$$

Lean4

noncomputable instance instBooleanAlgebra : BooleanAlgebra (L.DefinableSet A α) :=
  Function.Injective.booleanAlgebra (α := L.DefinableSet A α) _ Subtype.coe_injective coe_sup coe_inf coe_top coe_bot
    coe_compl coe_sdiff coe_himp

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