Theorems · Theorem · order theory
Set.inter_union_sdiff
∀ {α : Type u_1} (s t : Set α), s ∩ t ∪ s \ t = s- Defined in
- Mathlib.Order.BooleanAlgebra.Set
- Cited by
- 23 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.
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
- sup_inf_sdiffproof · cited by 13
Cited by23
Results whose statement or proof uses this declaration.
- Set.inter_union_complproof · cited by 14
- MeasureTheory.measure_le_inter_add_sdiffproof · cited by 7
- ProbabilityTheory.Kernel.rnDeriv_add_singularPartproof · cited by 7
- MeasureTheory.measure_inter_add_sdiff₀proof · cited by 6
- Set.ite_sameproof · cited by 5
- Set.InjOn.image_sdiffproof · cited by 3
- finprod_mem_inter_mul_sdiff'proof · cited by 3
- MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAtproof · cited by 3
- MeasurableEmbedding.variation_mapproof · cited by 3
- MeasureTheory.le_addContent_sdiffproof · cited by 2
- finsum_mem_inter_add_sdiff'proof · cited by 2
- Matroid.eRk_le_eRk_inter_add_eRk_sdiffproof · cited by 1