Theorems · Definition · measure theory

aeSeqSet

{ι : Sort u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        [inst_1 : MeasurableSpace β] →
          {f : ι → α → β} →
            {μ : MeasureTheory.Measure α} → (∀ (i : ι), AEMeasurable (f i) μ) → (α → (ι → β) → Prop) → Set α

If we have the additional hypothesis ∀ᵐ x ∂μ, p x (fun n ↦ f n x), this is a measurable set whose complement has measure 0 such that for all x ∈ aeSeqSet, f i x is equal to (hf i).mk (f i) x for all i and we have the pointwise property p x (fun n ↦ f n x).

Defined in

Mathlib.MeasureTheory.Function.AEMeasurableSequence

Cited by

16 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace