Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h : ∃ n, IndepSets (s n) s'
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι), s n
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h : ∃ n, IndepSets (s n) s'
⊢ IndepSets (⋂ (n : ι), s n) s'
intro t1 t2 ht1 ht2
case intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι), s n
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h : ∃ n, IndepSets (s n) s'
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι), s n
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
cases' h with n h
no goals
case intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι), s n
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
exact h t1 t2 (Set.mem_iInter.mp ht1 n) ht2