[Merged by Bors] - feat: pi-systems generating the product sigma algebra

[RemyDegenne]

We define pi-systems of cylinders and prove that they generate MeasurableSpace.pi.

Co-authored-by: Peter Pfaffelhuber
From the Kolmogorov extension theorem project.

---

[sgouezel]

I can't see lemmas relating cylinders and square cylinders (i.e., saying that a square cylinder is a cylinder, and that measurable square cylinders are also measurable cylinders). Are you planning to add those in a later PR? This could shorten a little bit the proof of the second inclusion in generateFrom_measurableCylinders, as you could deduce it from the monotonicity of generateFrom and generateFrom_squareCylinders.

bors d+
Thanks!

[bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

I hesitated between removing the square cylinders (as they are not used in the Kolmogorov extension proof), or adding the missing lemmas relating square cylinders and cylinders to this PR, or doing it in a later PR.
Let's not remove the square cylinders, which could be useful for something else, and add the missing lemmas in a later PR.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported