Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.approxOn

{α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : PseudoEMetricSpace α] →
        [OpensMeasurableSpace α] →
          [inst_3 : MeasurableSpace β] →
            (f : β → α) →
              Measurable f →
                (s : Set α) →
                  (y₀ : α) → y₀ ∈ s → [TopologicalSpace.SeparableSpace ↑s] → ℕ → MeasureTheory.SimpleFunc β α

Approximate a measurable function by a sequence of simple functions F n such that F n x ∈ s.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

39 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpaceMeasurableSpaceTopologicalSpace.SeparableSpace