neg — Mathlib

English

The negation of a finitely strongly measurable function is finitely strongly measurable when the target is a topological group with negation.

Русский

Отрицание финитной сильно измеримой функции является финитно сильно измеримой при наличии соответствующей структуры группы.

LaTeX

$$$\text{Subtractive}(f) \Rightarrow \text{FinStronglyMeasurable}(-f,\mu)$$$

Lean4

@[measurability]
protected theorem neg [SubtractionMonoid β] [ContinuousNeg β] (hf : FinStronglyMeasurable f μ) :
    FinStronglyMeasurable (-f) μ :=
  by
  refine ⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩
  suffices μ (Function.support fun x ↦ -(hf.approx n) x) < ∞ by convert this
  rw [Function.support_fun_neg (hf.approx n)]
  exact hf.fin_support_approx n

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