Theorems · Theorem · measure theory

Measurable.dite

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : (x : α) → Decidable (x ∈ s)] {f : ↑s → β},
  Measurable f →
    ∀ {g : ↑sᶜ → β}, Measurable g → MeasurableSet s → Measurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

Decidable