Theorem ProbabilityTheory.Kernel.integral_indicator₂

Modification history

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