Theorems · Inductive type · measure theory
MeasureTheory.SFinite
{α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → PropA measure is called s-finite if it is a countable sum of finite measures.
- Cited by
- 449 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by455
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.prod_prodstatement and proof · cited by 38
- MeasureTheory.Measure.prod_applystatement and proof · cited by 26
- MeasureTheory.lintegral_prodstatement and proof · cited by 20
- measurable_measure_prodMk_leftstatement and proof · cited by 20
- MeasureTheory.sfiniteSeqstatement and proof · cited by 20
- MeasureTheory.Measure.compProd_applystatement and proof · cited by 18
- MeasureTheory.Measure.measurePreserving_swapstatement and proof · cited by 16
- MeasureTheory.sum_sfiniteSeqstatement and proof · cited by 16
- MeasureTheory.Measure.prod_swapstatement and proof · cited by 14
- MeasureTheory.Measure.prod_restrictstatement and proof · cited by 12
- MeasureTheory.Measure.map_snd_prodstatement and proof · cited by 11
- MeasureTheory.Measure.snd_compProdstatement and proof · cited by 11
Showing the 200 most cited of 455.