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) \Rightarrow \text{AbsolutelyContinuousOnInterval}(f-g,a,b) $$$

Lean4

theorem sub (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
    AbsolutelyContinuousOnInterval (f - g) a b :=
  hf.fun_sub hg

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