Theorems · Theorem · measure theory
MeasureTheory.IntegrableOn.indicator
∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
MeasureTheory.IntegrableOn f s μ → MeasurableSet t → MeasureTheory.IntegrableOn (t.indicator f) s μ- Cited by
- 3 results in Mathlib
- Foundations
- Depth 204 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.
- 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
- Set.indicatorstatement · cited by 723
- MeasureTheory.IntegrableOnstatement and proof · cited by 548
- ESeminormedAddMonoidstatement and proof · cited by 133
- MeasureTheory.Integrable.indicatorproof · cited by 15
Cited by3
Results whose statement or proof uses this declaration.
- MeasureTheory.LocallyIntegrable.indicatorproof · cited by 2
- norm_sub_le_mul_volume_of_norm_deriv_le_of_leproof · cited by 1
- WeakFEPair.hf_modif_intproof · cited by 0