Theorems · Theorem · measure theory

Measurable.measurable_of_countable_ne

∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSingletonClass α], Measurable f → {x | f x ≠ g x}.Countable → Measurable g

If a function coincides with a measurable function outside of a countable set, it is measurable.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSingletonClass