Theorems · Theorem · measure theory

Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero

∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → ℝ} {x : X},
  Continuous f → HasCompactSupport f → 0 ≤ f → f x ≠ 0 → 0 < ∫ (x : X), f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

11 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.Measure.IsOpenPosMeasureMeasureTheory.IsFiniteMeasureOnCompacts