Theorems · Theorem · measure theory
MeasureTheory.lintegral_one
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ∫⁻ (x : α), 1 ∂μ = μ Set.univ- Cited by
- 14 results in Mathlib
- Foundations
- Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Set.univstatement and proof · cited by 3,945
- one_mulproof · cited by 2,841
- MeasureTheory.lintegralstatement · cited by 1,152
- MeasureTheory.lintegral_constproof · cited by 123
Cited by14
Results whose statement or proof uses this declaration.
- ProbabilityTheory.setLIntegral_preCDF_fstproof · cited by 4
- ProbabilityTheory.preCDF_le_oneproof · cited by 4
- ProbabilityTheory.integrable_toReal_condDistribproof · cited by 2
- MeasureTheory.Measure.bind_diracproof · cited by 2
- HasOuterApproxClosed.measure_le_lintegralproof · cited by 1
- measure_le_lintegral_thickenedIndicatorAuxproof · cited by 1
- MeasureTheory.absolutelyContinuous_of_isAddLeftInvariantproof · cited by 1
- MeasureTheory.absolutelyContinuous_of_isMulLeftInvariantproof · cited by 1
- MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicatorproof · cited by 1
- bergelson'proof · cited by 1
- ProbabilityTheory.integrable_preCDFproof · cited by 1
- ENNReal.lintegral_Lp_add_le_of_le_oneproof · cited by 1