Ω : Type u_1
ι : Type ?u.432097
s₁ s₂ : Set (Set Ω)
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h : IndepSets s₁ s₂
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.432097
s₁ s₂ : Set (Set Ω)
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h : IndepSets s₁ s₂
⊢ IndepSets s₂ s₁
intro t1 t2 ht1 ht2
Ω : Type u_1
ι : Type ?u.432097
s₁ s₂ : Set (Set Ω)
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h : IndepSets s₁ s₂
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ↑↑μ (t2 ∩ t1) = ↑↑μ t2 * ↑↑μ t1
Ω : Type u_1
ι : Type ?u.432097
s₁ s₂ : Set (Set Ω)
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h : IndepSets s₁ s₂
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
rw [Set.inter_comm, mul_comm]
no goals
Ω : Type u_1
ι : Type ?u.432097
s₁ s₂ : Set (Set Ω)
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h : IndepSets s₁ s₂
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ↑↑μ (t2 ∩ t1) = ↑↑μ t2 * ↑↑μ t1
exact h t2 t1 ht2 ht1