Theorems · Theorem · order theory
Set.disjoint_sdiff_left
∀ {α : Type u_1} {s t : Set α}, Disjoint (t \ s) s- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Disjointstatement · cited by 2,201
- disjoint_sdiff_self_leftproof · cited by 21
Cited by25
Results whose statement or proof uses this declaration.
- Matroid.Indep.contract_indep_iffproof · cited by 9
- Set.encard_sdiff_add_encard_of_subsetproof · cited by 6
- Set.disjoint_sdiff_interproof · cited by 4
- disjoint_memPartitionproof · cited by 3
- Set.encard_union_add_encard_interproof · cited by 3
- MeasureTheory.SignedMeasure.exists_compl_positive_negativeproof · cited by 2
- Matroid.contract_delete_contract'proof · cited by 2
- MeasureTheory.IsSetSemiring.mem_supClosure_iffproof · cited by 2
- Set.encard_sdiff_add_encardproof · cited by 2
- Set.Finite.ecard_lt_ecardproof · cited by 2
- Matroid.IsBasis.cardinalMk_eqproof · cited by 2
- Matroid.isBase_compl_iff_maximal_disjoint_isBaseproof · cited by 1