Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t)
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t)
refine' indepFun_iff_measure_inter_preimage_eq_mul.trans _
case mp
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h : ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t)

case mpr
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h : IndepSet (f ⁻¹' s) (g ⁻¹' t)
⊢ ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t)
constructor <;> intro h s t hs ht <;> specialize h s t hs ht
no goals
case mp
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h : ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t)
rwa [indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) μ]
no goals
case mpr
Ω : Type u_3
ι : Type ?u.3148409
β : Type u_1
β' : Type u_2
γ : Type ?u.3148418
γ' : Type ?u.3148421
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
h : IndepSet (f ⁻¹' s) (g ⁻¹' t)
⊢ ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) μ]