Theorems · Theorem · measure theory
MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {s : Set α},
MeasurableSet s → ∀ (t : Set α), μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)The measurable superset toMeasurable μ t of t (which has the same measure as t)
satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).
This only holds when μ is s-finite -- for example for σ-finite measures. For a version without
this assumption (but requiring that t has finite measure), see measure_toMeasurable_inter.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasureTheory.SFinite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · 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 · cited by 9,879
- MeasurableSetstatement and proof · cited by 3,075
- MeasureTheory.SFinitestatement and proof · cited by 449
- MeasureTheory.measure_ne_topproof · cited by 171
- MeasureTheory.toMeasurablestatement · cited by 77
- MeasureTheory.sfiniteSeqproof · cited by 20
- MeasureTheory.sum_sfiniteSeqproof · cited by 16
- MeasureTheory.Measure.measure_toMeasurable_inter_of_sumproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.restrict_toMeasurable_of_sFiniteproof · cited by 3
- VitaliFamily.ae_tendsto_measure_inter_divproof · cited by 2
- MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_oneproof · cited by 1
- norm_sub_le_mul_volume_of_norm_deriv_le_of_leproof · cited by 1