Theorems · Theorem · measure theory

Measurable.piecewise

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (s.piecewise f g)

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Basic

Cited by

9 results in Mathlib

Foundations

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