Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
hs' : ¬Set.Finite s
⊢ False
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
⊢ Set.Finite s
by_contra hs'
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
hs' : ¬Set.Finite s
⊢ False
simp [condCount, cond, Measure.count_apply_infinite hs'] at h