case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
⊢ IndepFun f' g'
rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
have h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A := hf.fun_comp A
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
h2 : g ⁻¹' B =ᵐ[μ] g' ⁻¹' B
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
have h2 : g ⁻¹' B =ᵐ[μ] g' ⁻¹' B := hg.fun_comp B
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
h2 : g ⁻¹' B =ᵐ[μ] g' ⁻¹' B
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
h2 : g ⁻¹' B =ᵐ[μ] g' ⁻¹' B
⊢ ↑↑μ (f' ⁻¹' A ∩ g' ⁻¹' B) = ↑↑μ (f' ⁻¹' A) * ↑↑μ (g' ⁻¹' B)
rw [← measure_congr h1, ← measure_congr h2, ← measure_congr (h1.inter h2)]
no goals
case intro.intro.intro.intro
Ω : Type u_2
ι : Type ?u.3257019
β : Type u_1
β' : Type ?u.3257025
γ : Type ?u.3257028
γ' : Type ?u.3257031
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β
g✝ : Ω → β'
mβ : MeasurableSpace β
f g f' g' : Ω → β
hfg : IndepFun f g
hf : f =ᵐ[μ] f'
hg : g =ᵐ[μ] g'
A : Set β
hA : MeasurableSet A
B : Set β
hB : MeasurableSet B
h1 : f ⁻¹' A =ᵐ[μ] f' ⁻¹' A
h2 : g ⁻¹' B =ᵐ[μ] g' ⁻¹' B
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
exact hfg _ _ ⟨_, hA, rfl⟩ ⟨_, hB, rfl⟩