English
The subtraction of a measurable function and a strongly measurable function is measurable.
Русский
Разность измеримой функции и сильно измеримой функции является измеримой.
LaTeX
$$$\forall g:\alpha \to E, \forall f:\alpha \to E, \text{Measurable } g \land \text{StronglyMeasurable } f \Rightarrow \text{Measurable } (x \mapsto g(x) - f(x))$$$
Lean4
/-- 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. -/
theorem _root_.Measurable.sub_stronglyMeasurable {α E : Type*} {_ : MeasurableSpace α} [AddGroup E] [TopologicalSpace E]
[MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [ContinuousNeg E] [PseudoMetrizableSpace E] {g f : α → E}
(hg : Measurable g) (hf : StronglyMeasurable f) : Measurable (g - f) :=
by
rw [sub_eq_add_neg]
exact hg.add_stronglyMeasurable hf.neg
