Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
h : ∃ n, n ∈ u ∧ IndepSets (s n) s'
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι) (_ : n ∈ u), 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 Ω
u : Set ι
h : ∃ n, n ∈ u ∧ IndepSets (s n) s'
⊢ IndepSets (⋂ (n : ι) (_ : n ∈ u), s n) s'
intro t1 t2 ht1 ht2
case intro.intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι) (_ : n ∈ u), s n
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
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 Ω
u : Set ι
h : ∃ n, n ∈ u ∧ IndepSets (s n) s'
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι) (_ : n ∈ u), s n
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
rcases h with ⟨n, hn, h⟩
no goals
case intro.intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ (n : ι) (_ : n ∈ u), s n
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2