Theorems · Theorem · measure theory
MeasureTheory.IntegrableOn.integrable_indicator
∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
MeasureTheory.IntegrableOn f s μ → MeasurableSet s → MeasureTheory.Integrable (s.indicator f) μ- Cited by
- 8 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasurableSetstatement and proof · cited by 3,075
- MeasureTheory.Integrablestatement · cited by 1,367
- Set.indicatorstatement · cited by 723
- MeasureTheory.IntegrableOnstatement and proof · cited by 548
- ESeminormedAddMonoidstatement and proof · cited by 133
- MeasureTheory.integrable_indicator_iffproof · cited by 30
Cited by8
Results whose statement or proof uses this declaration.
- MeasureTheory.integral_indicatorproof · cited by 38
- MeasureTheory.Integrable.indicatorproof · cited by 15
- MeasureTheory.BorelCantelli.integrable_processproof · cited by 1
- RealRMK.measure_le_of_isCompact_of_integralproof · cited by 1
- MeasureTheory.IntegrableOn.integrable_indicator₀proof · cited by 1
- MeasureTheory.integral_piecewiseproof · cited by 1