α : Type u_1
β : Type ?u.384442
γ : Type ?u.384445
δ : Type ?u.384448
ι : Type ?u.384451
R : Type ?u.384454
R' : Type ?u.384457
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ¬s = ∅
α : Type u_1
β : Type ?u.384442
γ : Type ?u.384445
δ : Type ?u.384448
ι : Type ?u.384451
R : Type ?u.384454
R' : Type ?u.384457
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ↑↑count s ≠ 0
rw [Ne.def, count_eq_zero_iff' s_mble]
no goals
α : Type u_1
β : Type ?u.384442
γ : Type ?u.384445
δ : Type ?u.384448
ι : Type ?u.384451
R : Type ?u.384454
R' : Type ?u.384457
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ¬s = ∅
exact hs'.ne_empty