Theorems · Definition · measure theory
MeasureTheory.Measure.FiniteAtFilter
{α : Type u_1} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → Filter α → PropA measure is called finite at filter f if it is finite at some set s ∈ f.
Equivalently, it is eventually finite at s in f.small_sets.
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Top.topproof · cited by 9,680
- Filterstatement and proof · cited by 8,121
Cited by37
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.finiteAt_nhdsstatement · cited by 10
- MeasureTheory.Measure.FiniteAtFilter.filter_monostatement and proof · cited by 6
- MeasureTheory.Measure.FiniteAtFilter.eventuallystatement and proof · cited by 4
- intervalIntegral.FTCFilter.finiteAt_innerstatement · cited by 4
- MeasureTheory.Measure.finiteAt_nhdsWithinstatement · cited by 3
- Filter.Tendsto.integral_sub_linear_isLittleO_aestatement and proof · cited by 3
- MeasureTheory.Measure.FiniteAtFilter.exists_mem_basisstatement and proof · cited by 3
- Filter.Tendsto.integrableAtFilterstatement · cited by 2
- MeasureTheory.Measure.FiniteAtFilter.inf_ae_iffstatement and proof · cited by 2
- intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae'statement and proof · cited by 2
- MeasureTheory.Measure.FiniteAtFilter.inf_of_leftstatement and proof · cited by 2
- intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'statement and proof · cited by 2