Commit 2024-03-13 15:40 e82ee277

feat: countable filtration in a countably generated measurable space (#10945) In a countably generated measurable space α, we can build a sequence of finer and finer finite measurable partitions of the space such that the measurable space is generated by the union of all partitions. This sequence of partitions (countablePartition α n) is defined in MeasureTheory.MeasurableSpace.CountablyGenerated. This is a new file in which we put the definition of CountablyGenerated (which was previously in MeasurableSpace.Basic). In Probability.Process.CountablyGenerated, we build the filtration generated by countablePartition α n for all n : ℕ, which we call countableFiltration α.