Theorems · Theorem · measure theory

measure_le_lintegral_thickenedIndicator

∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : PseudoEMetricSpace X] (μ : MeasureTheory.Measure X) {E : Set X},
  MeasurableSet E → ∀ {δ : ℝ} (δ_pos : 0 < δ), μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpace