Theorems · Theorem · measure theory

MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure

∀ {X : Type u_1} {E : Type u_2} [m : MeasurableSpace X] [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  (p : ENNReal) [one_le_p : Fact (1 ≤ p)] [p_ne_top : Fact (p ≠ ⊤)] {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) (c : E),
  {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p ⋯ hμs c = x}

If 𝒜 is a measure-dense family of sets and c : E, then the set of constant indicators with constant c whose underlying set is in 𝒜 is dense in the set of constant indicators which are in Lp E p μ when 1 ≤ p < ∞.

Defined in

Mathlib.MeasureTheory.Measure.SeparableMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupFactFact