case mp
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h : IndepFun f g
⊢ ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)

case mpr
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
⊢ IndepFun f g
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ IndepFun f g ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
constructor <;> intro h
no goals
case mp
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h : IndepFun f g
⊢ ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
refine' fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
case mpr.intro.intro.intro.intro
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
case mpr
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
⊢ IndepFun f g
rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
no goals
case mpr.intro.intro.intro.intro
Ω : Type u_3
ι : Type ?u.3034448
β : Type u_1
β' : Type u_2
γ : Type ?u.3034457
γ' : Type ?u.3034460
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ ↑↑μ (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑μ (f ⁻¹' s) * ↑↑μ (g ⁻¹' t)
exact h s t hs ht