fun_sub — Mathlib

English

If f and g are absolutely continuous on [a,b], then f-g is absolutely continuous on [a,b].

Русский

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

LaTeX

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

Lean4

theorem fun_sub (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
    AbsolutelyContinuousOnInterval (fun x ↦ f x - g x) a b :=
  by
  simp_rw [fun x ↦ show f x - g x = f x + (-(g x)) by abel]
  exact hf.fun_add (hg.fun_neg)

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