comp — Mathlib

English

For measurable f and g, IndepFun f g μ is equivalent to the statement that for all measurable s,t, IndepSet (f^{-1}(s)) (g^{-1}(t)) μ.

Русский

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

LaTeX

$$$IndepFun f g μ \iff ∀ s,t, MeasurableSet s → MeasurableSet t → IndepSet (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) (hg : ∀ i, Measurable (g i)) :
    iIndepFun (fun i ↦ g i ∘ f i) μ :=
  h.comp _ hg

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