Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < ↑↑(μ[|s]) t
rw [cond_apply _ hms]
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ (↑↑μ s)⁻¹ ≠ 0
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
refine' ENNReal.mul_pos _ hci
no goals
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ (↑↑μ s)⁻¹ ≠ 0
exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)