theorem
ProbabilityTheory.iIndepFun.reindex_three_abc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_three_acb
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₃, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_three_bac
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₂, Z₁, Z₃] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_three_bca
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₂, Z₃, Z₁] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_three_cab
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₃, Z₁, Z₂] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.reindex_three_cba
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
:
ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![Z₃, Z₂, Z₁] MeasureTheory.volume
theorem
ProbabilityTheory.iIndepFun.pair_last_of_three
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ) => hG) ![Z₁, Z₂, Z₃] MeasureTheory.volume)
(hZ₁ : Measurable Z₁)
(hZ₂ : Measurable Z₂)
(hZ₃ : Measurable Z₃)
:
ProbabilityTheory.IndepFun Z₁ (⟨Z₂, Z₃⟩) MeasureTheory.volume