Theorems · Definition · measure theory
MeasureTheory.spanningSetsIndex
{α : Type u_1} → {m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [MeasureTheory.SigmaFinite μ] → α → ℕspanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 185 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.SigmaFinitestatement and proof · cited by 526
- Nat.findproof · cited by 139
Cited by14
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.rnDeriv_lt_topproof · cited by 21
- MeasureTheory.mem_spanningSetsIndexstatement and proof · cited by 6
- MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'proof · cited by 3
- MeasureTheory.preimage_spanningSetsIndex_singletonstatement · cited by 2
- MeasureTheory.measure_singleton_lt_topproof · cited by 2
- MeasureTheory.mem_disjointed_spanningSetsIndexstatement · cited by 1
- MeasureTheory.mem_spanningSets_of_index_lestatement and proof · cited by 1
- MeasureTheory.eventually_mem_spanningSetsproof · cited by 1
- MeasureTheory.exists_pos_lintegral_lt_of_sigmaFiniteproof · cited by 1
- MeasureTheory.measurableSet_spanningSetsIndexstatement · cited by 1
- MeasureTheory.spanningSetsIndex_eq_iffstatement and proof · cited by 1
- VitaliFamily.exists_measurable_supersets_limRatioproof · cited by 1