Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t ∈ {s | MeasurableSet s}
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
⊢ Indep m' ⊥
intro s t _hs ht
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = Set.univ
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t ∈ {s | MeasurableSet s}
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
rw [Set.mem_setOf_eq, MeasurableSpace.measurableSet_bot_iff] at ht
case inl
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = ∅
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t

case inr
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = Set.univ
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = Set.univ
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
cases' ht with ht ht
no goals
case inl
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = ∅
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
rw [ht, Set.inter_empty, measure_empty, MulZeroClass.mul_zero]
no goals
case inr
Ω : Type u_1
ι : Type ?u.540154
m' m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s t : Set Ω
_hs : s ∈ {s | MeasurableSet s}
ht : t = Set.univ
⊢ ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
rw [ht, Set.inter_univ, measure_univ, mul_one]