Theorems · Definition · measure theory

MeasureTheory.Measure.aeEqSetoid

{α : Type u_1} →
  (β : Type u_2) →
    [inst : MeasurableSpace α] →
      [inst_1 : TopologicalSpace β] →
        (μ : MeasureTheory.Measure α) → Setoid { f // MeasureTheory.AEStronglyMeasurable f μ }

The equivalence relation of being almost everywhere equal for almost everywhere strongly measurable functions.

Defined in

Mathlib.MeasureTheory.Function.AEEqFun

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpace