[Merged by Bors] - feat: the sigma-algebra generated by a stochastic process is the coarsest that makes all its marginals measurable#39730

mathlib-splicebot[bot] wants to merge 1 commit into

masterleanprover-community/mathlib4:masterfrom

splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-Constructions.lean-78b8c598f1-b6u9l30leanprover-community/mathlib4_copy:splice-bot/pr-37259-Mathlib-MeasureTheory-MeasurableSpace-Constructions.lean-78b8c598f1-b6u9l30Copy head branch name to clipboard