English
Let f: Ω → β and g: Ω → β′ be independent with respect to μ. If φ: β → γ and ψ: β′ → γ′ are measurable, then φ ∘ f and ψ ∘ g are independent with respect to μ.
Русский
Пусть f: Ω → β и g: Ω → β′ — независимы относительно μ. Если φ: β → γ и ψ: β′ → γ′ измеримы, то φ ∘ f и ψ ∘ g независимы относительно μ.
LaTeX
$$$ \\operatorname{IndepFun}(f,g,\\mu) \\rightarrow \\operatorname{Measurable}(\\phi) \\rightarrow \\operatorname{Measurable}(\\psi) \\rightarrow \\operatorname{IndepFun}(\\phi \\circ f,\\ \\psi \\circ g) \\,\\mu $$$
Lean4
theorem comp {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'}
{φ : β → γ} {ψ : β' → γ'} (hfg : IndepFun f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
IndepFun (φ ∘ f) (ψ ∘ g) μ :=
Kernel.IndepFun.comp hfg hφ hψ
