∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α] [μ.IsOpenPosMeasure]
  {f : α → ℝ} {x : α}, Continuous f → MeasureTheory.Integrable f μ → 0 ≤ f → f x ≠ 0 → 0 < ∫ (x : α), f x ∂μ