theorem
ProbabilityTheory.iIndepFun.reindex_three_abc
{Ω : Type u_1}
[MeasureTheory.MeasureSpace Ω]
{G : Type u_2}
[hG : MeasurableSpace G]
{Z₁ Z₂ Z₃ : Ω → G}
(h_indep : iIndepFun ![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 : iIndepFun ![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 : iIndepFun ![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 : iIndepFun ![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 : iIndepFun ![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 : iIndepFun ![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 : iIndepFun ![Z₁, Z₂, Z₃] MeasureTheory.volume)
(hZ₁ : Measurable Z₁)
(hZ₂ : Measurable Z₂)
(hZ₃ : Measurable Z₃)
:
IndepFun Z₁ (⟨Z₂, Z₃⟩) MeasureTheory.volume