add — Mathlib

English

If h is HasIntegral for f and h' is HasIntegral for g, then HasIntegral holds for f+g and y+y'.

Русский

Если для f и g существуют интегралы y и y', то для f+g существует интеграл y+y'.

LaTeX

$$$\text{HasIntegral}(I,l,f,vol,y) \land \text{HasIntegral}(I,l,g,vol,y') \Rightarrow \text{HasIntegral}(I,l, f+g, vol, y+y')$$$

Lean4

nonrec theorem add (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 [HasIntegral, ← integralSum_add] using h.add h'

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