comp₀ — Mathlib

English

IndepFun f g μ is equivalent to the property that for all measurable s,t, μ(f^{-1}(s) ∩ g^{-1}(t)) = μ(f^{-1}(s)) μ(g^{-1}(t)).

Русский

IndepFun f g μ эквивалентно свойству, что для всех измеримых s,t выполняется μ(f^{-1}(s) ∩ g^{-1}(t)) = μ(f^{-1}(s)) μ(g^{-1}(t)).

LaTeX

$$$IndepFun f g μ \iff ∀ s,t, MeasurableSet s → MeasurableSet t → μ(f^{-1} s ∩ g^{-1} t) = μ(f^{-1} s) μ(g^{-1} t)$$$

Lean4

nonrec theorem comp₀ {β γ : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {mγ : ∀ i, MeasurableSpace (γ i)}
    {f : ∀ i, Ω → β i} (h : iIndepFun f μ) (g : ∀ i, β i → γ i) (hf : ∀ i, AEMeasurable (f i) μ)
    (hg : ∀ i, AEMeasurable (g i) (μ.map (f i))) : iIndepFun (fun i ↦ g i ∘ f i) μ :=
  h.comp₀ _ (by simp [hf]) (by simp [hg])

Похожие утверждения