sub — Mathlib

English

If f and g are AEFinStronglyMeasurable, then their difference f − g is AEFinStronglyMeasurable.

Русский

Если f и g — AEFinStronglyMeasurable, то их разность f − g — AEFinStronglyMeasurable.

LaTeX

$$$\text{AEFinStronglyMeasurable}(f, μ) \land \text{AEFinStronglyMeasurable}(g, μ) \Rightarrow \text{AEFinStronglyMeasurable}(f - g, μ).$$$

Lean4

@[measurability]
protected theorem sub [SubtractionMonoid β] [ContinuousSub β] (hf : AEFinStronglyMeasurable f μ)
    (hg : AEFinStronglyMeasurable g μ) : AEFinStronglyMeasurable (f - g) μ :=
  ⟨hf.mk f - hg.mk g, hf.finStronglyMeasurable_mk.sub hg.finStronglyMeasurable_mk, hf.ae_eq_mk.sub hg.ae_eq_mk⟩

Похожие утверждения