Theorems · Theorem · measure theory

Measurable.ite

∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop}
  {x : DecidablePred p},
  MeasurableSet {a | p a} → Measurable f → Measurable g → Measurable fun x_1 => if p x_1 then f x_1 else g x_1

This is slightly different from Measurable.piecewise. It can be used to show Measurable (ite (x=0) 0 1) by exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const, but replacing Measurable.ite by Measurable.piecewise in that example proof does not work.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Basic

Cited by

8 results in Mathlib

Foundations

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