neg — Mathlib

English

If f is AEFinStronglyMeasurable, then its pointwise negation −f is also AEFinStronglyMeasurable.

Русский

Если f — AEFinStronglyMeasurable, то и −f тоже AEFinStronglyMeasurable.

LaTeX

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

Lean4

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

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