Theorem ProbabilityTheory.Kernel.integral_integral_indicator

Modification history

2025-03-03 11:12
Mathlib/Probability/Kernel/SetIntegral.lean
feat: integrating the integral of an indicator (#22469) …
Added ProbabilityTheory.Kernel.integral_integral_indicatorView on Github →