4.12. Tactic.KernelHom.ForMathlib.LIntegral
Lebesgue integral utilities
This file provides helper lemmas for the Lebesgue integral with Dirac measures.
Main declarations
-
lintegral_lintegral_dirac: computing nested integrals with Dirac measures.
Module LeanMachineLearning.Tactic.KernelHom.ForMathlib.LIntegral contains 1 exposed declarations.