instBooleanAlgebra — Mathlib

English

The power set of a type α, with union, intersection, complement, difference, top, and bottom, forms a Boolean algebra.

Русский

Множество всех подмножеств типа α под операциями объединения, пересечения, дополнения, разности, верхнего и нижнего элементов образует булову алгебру.

LaTeX

$$$\mathcal{P}(\alpha) \text{ is a Boolean algebra with } \cup, \cap, ^c, \setminus, \emptyset, \alpha.$$$

Lean4

instance instBooleanAlgebra : BooleanAlgebra (Set α)
    where
  __ : DistribLattice (Set α) := inferInstance
  __ : BooleanAlgebra (α → Prop) := inferInstance
  compl := (·ᶜ)
  sdiff := (· \ ·)

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