Theorems · Theorem · order theory
sdiff_eq_left
∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint x y- Defined in
- Mathlib.Order.BooleanAlgebra.Basic
- Cited by
- 15 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Disjointstatement · cited by 2,201
- Eq.geproof · cited by 375
- GeneralizedBooleanAlgebrastatement and proof · cited by 204
- Disjoint.mono_leftproof · cited by 50
- disjoint_sdiff_self_leftproof · cited by 21
- Disjoint.sdiff_eq_leftproof · cited by 19
Cited by15
Results whose statement or proof uses this declaration.
- sdiff_eq_self_iff_disjointproof · cited by 4
- Matroid.delete_eq_self_iffproof · cited by 4
- sdiff_ltproof · cited by 2
- LowerSet.sdiff_eq_leftproof · cited by 2
- Ioc_sdiff_botSetproof · cited by 2
- SimpleGraph.CliqueFree.mem_of_sup_edge_isNCliqueproof · cited by 2
- disjointed_eq_selfproof · cited by 1
- Finset.sdiff_eq_self_iff_disjointproof · cited by 1
- Matroid.Indep.closure_sdiff_ssubsetproof · cited by 1
- SimpleGraph.edgeSet_fromEdgeSet_incidenceSetproof · cited by 1
- Matroid.delete_contract_deleteproof · cited by 0
- SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_unionproof · cited by 0