theorem MeasurableSpace.comap_pi {δ : Type u_1} {X : δ → Type u_2} [m : (a : δ) → MeasurableSpace (X a)] {α : Type u_3} {g : α → (a : δ) → X a} : MeasurableSpace.comap g pi = ⨆ (a : δ), MeasurableSpace.comap (fun (x : α) => g x a) (m a)

theorem ProbabilityTheory.indepFun_proj_infinitePi_infinitePi {ι : Type u_1} {κ : Type u_2} {𝓧 : ι → κ → Type u_3} [m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)] {μ : (i : ι) → (j : κ) → MeasureTheory.Measure (𝓧 i j)} [∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)] {a b : κ} (h : a ≠ b) : IndepFun (fun (ω : (i : ι) → (i_1 : κ) → 𝓧 i i_1) (i : ι) => ω i a) (fun (ω : (i : ι) → (i_1 : κ) → 𝓧 i i_1) (i : ι) => ω i b) (MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.infinitePi (μ i))