Theorems · Theorem · measure theory

aemeasurable_of_unif_approx

∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_3} [inst_1 : MeasurableSpace β] [inst_2 : PseudoMetricSpace β]
  [BorelSpace β] {μ : MeasureTheory.Measure α} {g : α → β},
  (∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε) → AEMeasurable g μ

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpacePseudoMetricSpaceBorelSpace