no goals
Ω : Type u_1
ι : Type ?u.2709210
s t : Set Ω
S T : Set (Set Ω)
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : autoParam (MeasureTheory.Measure Ω) _auto✝
inst✝ : IsProbabilityMeasure μ
h : IndepSets {s} {t}
u : Set Ω
hu : u ∈ {s}
⊢ MeasurableSet u
rwa [Set.mem_singleton_iff.mp hu]
no goals
Ω : Type u_1
ι : Type ?u.2709210
s t : Set Ω
S T : Set (Set Ω)
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : autoParam (MeasureTheory.Measure Ω) _auto✝
inst✝ : IsProbabilityMeasure μ
h : IndepSets {s} {t}
u : Set Ω
hu : u ∈ {t}
⊢ MeasurableSet u
rwa [Set.mem_singleton_iff.mp hu]