fun_neg — Mathlib

English

If f is absolutely continuous on [a,b], then its negation -f is absolutely continuous on [a,b].

Русский

Если f абсолютно непрерывна на [a,b], то -f тоже абсолютно непрерывна на [a,b].

LaTeX

$$$ \text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(-f,a,b) $$$

Lean4

theorem fun_neg (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun x ↦ -(f x)) a b :=
  by
  apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf)
  · exact Finset.sum_nonneg (fun i hi ↦ by positivity)
  · simp

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