iIndepFun_precomp_of_bijective — Mathlib

English

Independence is preserved under bijective reindexing: iIndepFun f μ is equivalent to iIndepFun (f ∘ g) μ for a bijection g.

Русский

Независимость сохраняется при биективной переиндексации: iIndepFun f μ эквивалентно iIndepFun (f ∘ g) μ при биекции g.

LaTeX

$$$ \\operatorname{iIndepFun} f μ \\iff \\operatorname{iIndepFun} (\\lambda i \\mapsto f (g i)) μ$, \n \\text{ если } g \\text{ Bijective }$$

Lean4

theorem iIndepFun_precomp_of_bijective {g : ι' → ι} (hg : g.Bijective) :
    iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ ↔ iIndepFun f μ
    where
  mp := .of_precomp hg.surjective
  mpr := .precomp hg.injective

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