instGeneralizedBooleanAlgebra — Mathlib

English

The collection of finite subsets of α, with union, intersection, and SDiff, forms a generalized Boolean algebra.

Русский

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

LaTeX

$$$ \\mathrm{Finset}(\\alpha) \text{ equipped with } \\cup, \\cap, \\setminus \text{ is a generalized Boolean algebra}. $$$

Lean4

instance : GeneralizedBooleanAlgebra (Finset α)
    where
  sup_inf_sdiff := by grind
  inf_inf_sdiff := by grind

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