English
Let h be HasIntegral for f and y, and h' be HasIntegral for g and y'. Then the difference f − g has HasIntegral with value y − y'.
Русский
Пусть для функций f, g существует интеграл в рамках данного прямоугольника I с параметрами l и вещественной областью vol: f имеет значение интеграла y, g имеет значение y'. Тогда функция f − g имеет интеграл с значением y − y'.
LaTeX
$$$\text{HasIntegral } I\ l\ f\ vol\ y \quad\text{и}\quad \text{HasIntegral } I\ l\ g\ vol\ y'\ \Rightarrow\ \text{HasIntegral } I\ l\ (f - g)\ vol\ (y - y')$$$
Lean4
theorem sub (h : HasIntegral I l f vol y) (h' : HasIntegral I l g vol y') : HasIntegral I l (f - g) vol (y - y') := by
simpa only [sub_eq_add_neg] using h.add h'.neg
