Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.tendsto_approxOn

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] {x : β},
  f x ∈ closure s →
    Filter.Tendsto (fun n => (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop (nhds (f x))

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpaceMeasurableSpaceTopologicalSpace.SeparableSpace