integral_add — Mathlib

English

In a complete space, Integrable is equivalent to the Cauchy criterion for integral sums across all partitions and base radii r.

Русский

В полном пространстве интегрируемость эквивалентна критерию Коши для интегральных сумм на всех разбиениях и радиусах базы r.

LaTeX

$$$\mathrm{integrable\_iff\_cauchy\_basis}(I,l,f,vol) \iff \text{Cauchy}((l.toFilteriUnion I ⊤).map (\mathrm{integralSum} f vol))$$$

Lean4

theorem integral_add (hf : Integrable I l f vol) (hg : Integrable I l g vol) :
    integral I l (f + g) vol = integral I l f vol + integral I l g vol :=
  (hf.hasIntegral.add hg.hasIntegral).integral_eq

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