Theorems · Definition · measure theory

AEMeasurable.mk

{α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      [inst : MeasurableSpace β] → {μ : MeasureTheory.Measure α} → (f : α → β) → AEMeasurable f μ → α → β

Given an almost everywhere measurable function f, associate to it a measurable function that coincides with it almost everywhere. f is explicit in the definition to make sure that it shows in pretty-printing.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

75 results in Mathlib

Foundations

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

Assumes

MeasurableSpace