Theorems · Inductive type · order theory
GeneralizedBooleanAlgebra
Type u → Type u
A generalized Boolean algebra is a distributive lattice with ⊥ and a relative complement
operation \ (called sdiff, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a and
(a ⊓ b) ⊓ (a \ b) = ⊥, i.e. a \ b is the complement of b in a.
This is a generalization of Boolean algebras which applies to Finset α for arbitrary
(not-necessarily-Fintype) α.
- Defined in
- Mathlib.Order.BooleanAlgebra.Defs
- Cited by
- 204 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by231
Results whose statement or proof uses this declaration.
- disjointedstatement and proof · cited by 64
- Finset.diffsstatement and proof · cited by 37
- disjoint_disjointedstatement and proof · cited by 25
- disjoint_sdiff_self_rightstatement and proof · cited by 22
- disjoint_sdiff_self_leftstatement and proof · cited by 21
- UV.compressstatement and proof · cited by 20
- sdiff_sdiff_right_selfstatement and proof · cited by 20
- UV.compressionstatement and proof · cited by 15
- sdiff_eq_leftstatement and proof · cited by 15
- sup_inf_sdiffstatement and proof · cited by 13
- UV.mem_compressionstatement and proof · cited by 9
- inf_inf_sdiffstatement and proof · cited by 8
Showing the 200 most cited of 231.