Theorems · Definition · measure theory

MeasureTheory.AEEqFun

(α : Type u_1) →
  (β : Type u_2) → [inst : MeasurableSpace α] → [TopologicalSpace β] → MeasureTheory.Measure α → Type (max u_1 u_2)

The space of equivalence classes of almost everywhere strongly measurable functions, where two strongly measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

Defined in

Mathlib.MeasureTheory.Function.AEEqFun

Cited by

856 results in Mathlib

Foundations

Depth 174 from the axioms, rests on 4,667 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpace