SetIntegral

📁 Source: Mathlib/Probability/Kernel/SetIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems integral_integral_indicator	1
Total	1

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_integral_indicator 📖	mathematical	MeasurableSet	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.Measure.restrict	—	MeasureTheory.integral_indicator integral_indicator₂

---

← Back to Index