English
If g is surjective, independence of the f-family after composing with g implies independence of the original f-family.
Русский
Если g сюръективна, независимость семейства f после композиции f ∘ g влечет за собой независимость исходного семейства f.
LaTeX
$$$ \\text{Function.Surjective}(g) \\rightarrow \\operatorname{iIndepFun} (m := m \\circ g) (\\lambda i \\mapsto f (g i)) μ \\rightarrow \\operatorname{iIndepFun} f μ$$$
Lean4
theorem precomp {g : ι' → ι} (hg : g.Injective) (h : iIndepFun f μ) :
iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ :=
by
have : IsProbabilityMeasure μ := h.isProbabilityMeasure
nontriviality ι'
have A (x) : Function.invFun g (g x) = x := Function.leftInverse_invFun hg x
rw [iIndepFun_iff] at h ⊢
intro t s' hs'
simpa [A] using h (t.map ⟨g, hg⟩) (f' := fun i ↦ s' (invFun g i)) (by simpa [A] using hs')
