Theorems · Definition · measure theory
MeasureTheory.sfiniteSeq
{α : Type u_1} →
{m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [h : MeasureTheory.SFinite μ] → ℕ → MeasureTheory.Measure αA sequence of finite measures such that μ = sum (sfiniteSeq μ) (see sum_sfiniteSeq).
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 193 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.
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.SFinitestatement and proof · cited by 449
- MeasureTheory.SFinite.out'proof · cited by 1
Cited by20
Results whose statement or proof uses this declaration.
- measurable_measure_prodMk_leftproof · cited by 20
- MeasureTheory.sum_sfiniteSeqstatement · cited by 16
- MeasureTheory.Measure.prod_swapproof · cited by 14
- MeasureTheory.Measure.prod_restrictproof · cited by 12
- MeasureTheory.Measure.map_prod_mapproof · cited by 7
- MeasureTheory.Measure.measure_toMeasurable_inter_of_sFiniteproof · cited by 4
- MeasureTheory.exists_isFiniteMeasure_absolutelyContinuousproof · cited by 4
- MeasureTheory.Measure.prod_diracproof · cited by 3
- MeasureTheory.Measure.dirac_prodproof · cited by 3
- MeasureTheory.Measure.prod_addproof · cited by 2
- MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀proof · cited by 2
- MeasureTheory.sfiniteSeq_lestatement and proof · cited by 2