Commit 2024-10-27 19:30 b420076a

View on Github →

chore(MeasureTheory/Constructions/Prod/Basic: split (#18286) There were two things going on in this file:

  • Measurability according to the product sigma-algebra
  • The product measure The former can be defined much earlier than the latter, in particular without importing Measure.

Estimated changes

added theorem generateFrom_eq_prod
added theorem generateFrom_prod
added theorem generateFrom_prod_eq
added theorem isPiSystem_prod
deleted theorem IsCountablySpanning.prod
deleted theorem IsPiSystem.prod
deleted theorem generateFrom_eq_prod
deleted theorem generateFrom_prod
deleted theorem generateFrom_prod_eq
deleted theorem isPiSystem_prod
modified theorem IsPiSystem.insert_empty
modified theorem IsPiSystem.insert_univ
added theorem IsPiSystem.prod
modified theorem IsPiSystem.singleton
modified def IsPiSystem
modified inductive generatePiSystem
modified theorem generatePiSystem_eq
modified theorem generatePiSystem_mono
modified theorem isPiSystem_generatePiSystem