Commit 2024-11-04 01:54 eb291632

View on Github →

chore: make generateFrom_induction dependent and stronger (#17860) Incidentally, this makes it usable in the induction/induction' tactics. From GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

modified theorem MeasurableSpace.generateFrom_induction

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/MeasureTheory/SetAlgebra.lean

Modified Mathlib/Probability/Independence/Kernel.lean