Theorems · Theorem · measure theory

Measurable.stronglyMeasurable_add

∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddCancelMonoid E] [inst_1 : TopologicalSpace E]
  [inst_2 : MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [TopologicalSpace.PseudoMetrizableSpace E]
  {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (f + g)

In a normed vector space, the addition of a strongly measurable function and a measurable function is measurable. Note that this is not true without further second-countability assumptions for the addition of two measurable functions.

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCancelMonoidTopologicalSpaceMeasurableSpaceBorelSpaceContinuousAddTopologicalSpace.PseudoMetrizableSpace