Theorems · Theorem · measure theory

Measurable.sub_stronglyMeasurable

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

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

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceMeasurableSpaceBorelSpaceContinuousAddContinuousNegTopologicalSpace.PseudoMetrizableSpace