feat: the sigma-algebra generated by a stochastic process is the coarsest that makes all its marginals measurable (leanprover-community#39730)

This PR was automatically created from PR leanprover-community#37259 by @EtienneC30 via a [review comment](leanprover-community#37259 (comment)) by @EtienneC30.

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

Author: 2 people

Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

@@ -586,6 +586,12 @@ theorem measurable_pi_lambda (f : α → ∀ a, X a) (hf : ∀ a, Measurable fun
     Measurable f :=
   measurable_pi_iff.mpr hf
 
+lemma MeasurableSpace.comap_process_pi (X : (a : δ) → β → X a) :
+    MeasurableSpace.comap (fun b a ↦ X a b) inferInstance =
+      ⨆ a, MeasurableSpace.comap (X a) inferInstance := by
+  simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
+  rfl
+
 /-- The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable. -/
 @[fun_prop]
 theorem measurable_update' {a : δ} [DecidableEq δ] :