Ω : Type u_1
ι : Type ?u.108607
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
h_0_1_top : ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
Ω : Type u_1
ι : Type ?u.108607
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
have h_0_1_top := measure_eq_zero_or_one_or_top_of_indepSet_self h_indep
no goals
Ω : Type u_1
ι : Type ?u.108607
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
h_0_1_top : ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
simpa [measure_ne_top μ] using h_0_1_top