Ω : Type u_1
ι : Type ?u.648825
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥
Ω : Type u_1
ι : Type ?u.648825
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : Set Ω
⊢ IndepSet s ∅
simp only [IndepSet, generateFrom_singleton_empty]
no goals
Ω : Type u_1
ι : Type ?u.648825
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥
exact indep_bot_right _