Theorems · Theorem · measure theory
MeasureTheory.measure_sdiff_null
∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
{s t : Set α}, μ t = 0 → μ (s \ t) = μ s- Defined in
- Mathlib.MeasureTheory.OuterMeasure.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- ENNRealstatement and proof · cited by 9,879
- FunLikestatement and proof · cited by 2,560
- zero_addproof · cited by 2,366
- le_reflproof · cited by 2,061
- add_le_addproof · cited by 666
- LE.le.antisymmproof · cited by 507
- MeasureTheory.measure_monoproof · cited by 338
- Set.inter_subset_rightproof · cited by 329
- Set.sdiff_subsetproof · cited by 156
- MeasureTheory.OuterMeasureClassstatement and proof · cited by 104
Cited by13
Results whose statement or proof uses this declaration.
- MeasureTheory.measure_le_setAverage_posproof · cited by 5
- MeasureTheory.exists_null_frontier_thickeningproof · cited by 3
- MeasureTheory.measure_le_setLAverage_posproof · cited by 2
- MeasureTheory.exists_notMem_null_laverage_leproof · cited by 2
- MeasureTheory.exists_notMem_null_le_averageproof · cited by 2
- MeasureTheory.Measure.ae_mem_finset_iffproof · cited by 2
- MeasureTheory.measure_setLAverage_le_posproof · cited by 2
- MeasureTheory.Measure.toSphere_apply_univproof · cited by 2
- MeasureTheory.Measure.map_eq_comapproof · cited by 1
- MeasureTheory.measure_inter_conullproof · cited by 1
- MeasureTheory.Conservative.frequently_measure_inter_ne_zeroproof · cited by 1
- MeasureTheory.exists_notMem_null_le_laverageproof · cited by 1