Theorems · Theorem · measure theory

Measurable.simpleFunc_add

∀ {α : Type u_1} {E : Type u_5} {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddCancelMonoid E]
  [MeasurableAdd E] {g : α → E}, Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (⇑f + g)

In a topological vector space, the addition of a simple function and a measurable function is measurable.

Defined in

Mathlib.MeasureTheory.Function.SimpleFunc

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceAddCancelMonoidMeasurableAdd