Theorems · Definition · measure theory
MeasureTheory.spanningSets
{α : Type u_1} → {m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SigmaFinite μ] → ℕ → Set αA noncomputable way to get a monotone collection of sets that span univ and have finite
measure using Classical.choose. This definition satisfies monotonicity in addition to all other
properties in SigmaFinite.
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasureTheory.SigmaFinite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.SigmaFinitestatement and proof · cited by 526
- Set.accumulateproof · cited by 32
- MeasureTheory.Measure.toFiniteSpanningSetsInproof · cited by 13
- MeasureTheory.Measure.FiniteSpanningSetsIn.setproof · cited by 10
Cited by45
Results whose statement or proof uses this declaration.
- MeasureTheory.measure_spanningSets_lt_topstatement · cited by 25
- MeasureTheory.measurableSet_spanningSetsstatement · cited by 21
- MeasureTheory.Measure.rnDeriv_lt_topproof · cited by 21
- MeasureTheory.iUnion_spanningSetsstatement · cited by 19
- MeasureTheory.monotone_spanningSetsstatement · cited by 8
- MeasureTheory.Measure.add_right_injproof · cited by 7
- MeasureTheory.mem_spanningSetsIndexstatement and proof · cited by 6
- ConvexOn.map_condExp_leproof · cited by 4
- MeasureTheory.isCountablySpanning_spanningSetsstatement and proof · cited by 4
- MeasureTheory.sigmaFiniteTrim_monoproof · cited by 4
- MeasureTheory.SigmaFinite.of_mapproof · cited by 4
- MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFiniteproof · cited by 3