Commit 2024-12-14 15:50 e2b32447

View on Github →

chore: make some induction_on* compatible with induction (#19898)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

modified theorem MeasurableSet.induction_on_open

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/PiSystem.lean

modified theorem MeasurableSpace.induction_on_inter

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Topology/Baire/BaireMeasurable.lean

added theorem closure_residualEq

added theorem coborder_mem_residual