case intro.intro.intro.intro
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ ↑↑μ (φ ∘ f ⁻¹' A ∩ ψ ∘ g ⁻¹' B) = ↑↑μ (φ ∘ f ⁻¹' A) * ↑↑μ (ψ ∘ g ⁻¹' B)
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
⊢ IndepFun (φ ∘ f) (ψ ∘ g)
rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
case intro.intro.intro.intro.a
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ φ ∘ f ⁻¹' A ∈ {s | MeasurableSet s}

case intro.intro.intro.intro.a
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ ψ ∘ g ⁻¹' B ∈ {s | MeasurableSet s}
case intro.intro.intro.intro
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ ↑↑μ (φ ∘ f ⁻¹' A ∩ ψ ∘ g ⁻¹' B) = ↑↑μ (φ ∘ f ⁻¹' A) * ↑↑μ (ψ ∘ g ⁻¹' B)
apply hfg
no goals
case intro.intro.intro.intro.a
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ φ ∘ f ⁻¹' A ∈ {s | MeasurableSet s}
exact ⟨φ ⁻¹' A, hφ hA, Set.preimage_comp.symm⟩
no goals
case intro.intro.intro.intro.a
Ω : Type u_5
ι : Type ?u.3311612
β : Type u_1
β' : Type u_2
γ : Type u_3
γ' : Type u_4
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g
hφ : Measurable φ
hψ : Measurable ψ
A : Set γ
hA : MeasurableSet A
B : Set γ'
hB : MeasurableSet B
⊢ ψ ∘ g ⁻¹' B ∈ {s | MeasurableSet s}
exact ⟨ψ ⁻¹' B, hψ hB, Set.preimage_comp.symm⟩