Theorems · Theorem · measure theory

RealRMK.exists_open_approx

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (f : CompactlySupportedContinuousMap X ℝ) {ε : ℝ},
  0 < ε →
    ∀ (E : Set X) {μ : MeasureTheory.Content X},
      μ.outerMeasure E ≠ ⊤ →
        MeasurableSet E →
          ∀ {c : ℝ},
            (∀ x ∈ E, f x < c) → ∃ V, E ⊆ ↑V ∧ (∀ x ∈ V, f x < c) ∧ μ.measure ↑V ≤ μ.measure E + ENNReal.ofReal ε

Given a set E, a function f : C_c(X, ℝ), 0 < ε and ∀ x ∈ E, f x < c, there exists an open set V such that E ⊆ V and the sets are similar in measure and ∀ x ∈ V, f x < c.

Defined in

Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceMeasurableSpaceBorelSpace