Structures · Analysis
MeasureTheory.SigmaFinite
A measure μ is called σ-finite if there is a countable collection of sets
{ A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.
- Shape
- One type argument · adds out'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every MeasureTheory.SigmaFinite is also a
Provided automatically by
Concrete types that are instances5
- UpperHalfPlane
- List.TProd
- Prod
- Set.Elem
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by500
- MeasureTheory.spanningSets
- MeasureTheory.Measure.pi_pi
- MeasureTheory.condExpL1
- MeasureTheory.measure_spanningSets_lt_top
- MeasureTheory.Measure.rnDeriv_lt_top
- MeasureTheory.condExp_of_stronglyMeasurable
- MeasureTheory.measurableSet_spanningSets
- MeasureTheory.iUnion_spanningSets
- MeasureTheory.Measure.pi_eq
- MeasureTheory.condExpInd
- MeasureTheory.spanningSetsIndex
- MeasureTheory.dominatedFinMeasAdditive_condExpInd
- MeasureTheory.Measure.rnDeriv_withDensity
- MeasureTheory.Measure.toFiniteSpanningSetsIn
- MeasureTheory.setIntegral_condExp
- MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
- MeasureTheory.condExpIndL1Fin
- MeasureTheory.Measure.prod_eq
- MeasureTheory.condExpL1CLM
- MeasureTheory.condExpIndL1
- MeasureTheory.Measure.ae_eq_set_pi
- MeasureTheory.Measure.addHaarMeasure_unique
- MeasureTheory.condExp_ae_eq_condExpL1
- MeasureTheory.withDensity_eq_iff_of_sigmaFinite
- MeasureTheory.setLIntegral_condLExp
- MeasureTheory.Measure.rnDeriv_add'
- MeasureTheory.condExp_restrict_ae_eq_restrict
- MeasureTheory.monotone_spanningSets
- MeasureTheory.Measure.add_right_inj
- MeasureTheory.measurePreserving_piCongrLeft
- MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
- MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite
- MeasureTheory.Measure.rnDeriv_self
- MeasureTheory.mem_spanningSetsIndex
- MeasureTheory.condExp_condExp_of_le
- MeasureTheory.lintegral_condLExp
- MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
- MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
- MeasureTheory.Measure.rnDeriv_ne_top
- MeasureTheory.aestronglyMeasurable_condExpL1
- MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
- MeasureTheory.ae_eq_condLExp
- MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
- MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le
- MeasureTheory.condExpInd_ae_eq_condExpIndSMul
- MeasureTheory.condExp_of_sigmaFinite
- MeasureTheory.Measure.eq_rnDeriv₀
- MeasureTheory.volume_pi_pi
- MeasureTheory.integral_rnDeriv_smul
- MeasureTheory.integral_condExp