Commit 2025-01-07 08:13 eb9d83a3

View on Github →

chore(Measure/Pi): move parts to MeasurableSpace/ (#20215)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

deleted theorem IsCountablySpanning.pi

deleted theorem IsPiSystem.pi

deleted theorem MeasurableSpace.pi_eq_generateFrom_projections

deleted theorem generateFrom_eq_pi

deleted theorem generateFrom_pi

deleted theorem generateFrom_pi_eq

deleted theorem isPiSystem_pi

Created Mathlib/MeasureTheory/MeasurableSpace/Pi.lean

added theorem IsCountablySpanning.pi

added theorem IsPiSystem.pi

added theorem MeasurableSpace.pi_eq_generateFrom_projections

added theorem generateFrom_eq_pi

added theorem generateFrom_pi

added theorem generateFrom_pi_eq

added theorem isPiSystem_pi

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/Kernel.lean