Theorems · Theorem · measure theory
MeasureTheory.measure_sdiff
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
s₂ ⊆ s₁ → MeasureTheory.NullMeasurableSet s₂ μ → μ s₂ ≠ ⊤ → μ (s₁ \ s₂) = μ s₁ - μ s₂- Cited by
- 20 results in Mathlib
- Foundations
- Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- MeasureTheory.NullMeasurableSetstatement and proof · cited by 337
- Set.union_eq_self_of_subset_rightproof · cited by 25
- MeasureTheory.measure_sdiff'proof · cited by 4
Cited by20
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.IndepSets.indepproof · cited by 9
- MeasureTheory.measure_sdiff_lt_of_lt_addproof · cited by 8
- MeasureTheory.measure_sdiff_le_iff_le_addproof · cited by 3
- ProbabilityTheory.Kernel.setIntegral_densityproof · cited by 2
- MeasureTheory.Measure.ext_of_Iicproof · cited by 2
- ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finiteproof · cited by 1
- MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finiteproof · cited by 1
- NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOneproof · cited by 1
- ProbabilityTheory.setLIntegral_toKernel_prodproof · cited by 1
- ProbabilityTheory.Kernel.IndepSets.indep_auxproof · cited by 1
- MeasureTheory.tendsto_setIntegral_of_monotone₀proof · cited by 1