Theorems · Theorem · order theory
inf_sdiff
∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], (x ⊓ y) \ z = x \ z ⊓ y \ z- Defined in
- Mathlib.Order.BooleanAlgebra.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GeneralizedBooleanAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botproof · cited by 4,720
- GeneralizedBooleanAlgebrastatement and proof · cited by 204
- inf_commproof · cited by 139
- sup_eq_leftproof · cited by 71
- inf_le_infproof · cited by 54
- sdiff_leproof · cited by 36
- inf_sup_rightproof · cited by 26
- sup_inf_leftproof · cited by 22
- sup_inf_rightproof · cited by 22
- inf_bot_eqproof · cited by 14
- bot_inf_eqproof · cited by 11
- sdiff_uniqueproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- Set.sdiff_inter_distrib_rightproof · cited by 3
- Finset.inf_sdiff_rightproof · cited by 1