Theorems · Theorem · logic and foundations
Set.sdiff_eq
∀ {α : Type u} (s t : Set α), s \ t = s ∩ tᶜ- Defined in
- Mathlib.Data.Set.Operations
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Compl.complstatement · cited by 2,925
Cited by59
Results whose statement or proof uses this declaration.
- Set.sdiff_eq_compl_interproof · cited by 17
- frontier_eq_closure_inter_closureproof · cited by 12
- MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrictproof · cited by 6
- hasDerivWithinAt_iff_tendsto_slopeproof · cited by 6
- MeasureTheory.Measure.eq_singularPartproof · cited by 6
- Matroid.IsBasis'.contract_eq_contract_deleteproof · cited by 5
- HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNEproof · cited by 4
- MeasureTheory.Measure.restrict_inter_add_sdiff₀proof · cited by 4
- accPt_principal_iff_clusterPtproof · cited by 4
- hasFDerivWithinAt_congr_set_nhdsNEproof · cited by 4
- MeasureTheory.OuterMeasure.isCaratheodory_complproof · cited by 4
- Matroid.delete_contract_eq_sdiffproof · cited by 3