Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (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 ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
⊢ IndepSets (⋃ (n : ι) (_ : n ∈ u), s n) s'
intro t1 t2 ht1 ht2
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ i i_1, t1 ∈ s i
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
t1 t2 : Set Ω
ht1 : t1 ∈ ⋃ (n : ι) (_ : n ∈ u), s n
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
simp_rw [Set.mem_iUnion] at ht1
case intro.intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ i i_1, t1 ∈ s i
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
rcases ht1 with ⟨n, hpn, ht1⟩
no goals
case intro.intro
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
s : ι → Set (Set Ω)
s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
u : Set ι
hyp : ∀ (n : ι), n ∈ u → IndepSets (s n) s'
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
exact hyp n hpn t1 t2 ht1 ht2