Theorems · Theorem · measure theory

Measurable.find

∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {x : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop}
  [inst : (n : ℕ) → DecidablePred (p n)],
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), MeasurableSet {x | p n x}) → ∀ (h : ∀ (x : α), ∃ n, p n x), Measurable fun x => f (Nat.find ⋯) x

A piecewise function on countably many pieces is measurable if all the data is measurable.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidablePred