Theorems · Inductive type · measure theory
MeasureTheory.IsLocallyFiniteMeasure
{α : Type u_1} → {m0 : MeasurableSpace α} → [TopologicalSpace α] → MeasureTheory.Measure α → PropA measure is called locally finite if it is finite in some neighborhood of each point.
- Cited by
- 171 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by181
Results whose statement or proof uses this declaration.
- Continuous.intervalIntegrablestatement and proof · cited by 32
- ContinuousOn.intervalIntegrablestatement and proof · cited by 27
- MeasureTheory.Measure.toBoxAdditivestatement and proof · cited by 22
- IsUnifLocDoublingMeasure.vitaliFamilystatement · cited by 13
- VitaliFamily.limRatioMeasstatement and proof · cited by 11
- MeasureTheory.Measure.finiteAt_nhdsstatement and proof · cited by 10
- intervalIntegrable_conststatement and proof · cited by 10
- measure_Icc_lt_topstatement and proof · cited by 5
- ContinuousOn.intervalIntegrable_of_Iccstatement and proof · cited by 5
- ContDiffBump.support_normed_eqstatement and proof · cited by 5
- MeasureTheory.Measure.toBoxAdditive_applystatement and proof · cited by 5
- VitaliFamily.measure_le_of_frequently_lestatement and proof · cited by 5