integrable_iff_cauchy — Mathlib

English

In a complete space, Integrable I l f vol is equivalent to the integral sums forming a Cauchy net with respect to the basis filter; i.e., the net of integral sums is Cauchy in F.

Русский

В полном пространстве Integrable I l f vol эквивалентно тому, что сеть интегральных сумм образует схождение по базисному фильтру; сама сеть сумм интеграла является цuх последовательной в F.

LaTeX

$$$\mathrm{Integrable}(I,l,f,vol) \iff \mathrm{Cauchy}\bigl((l.toFilteriUnion I \top).map (\mathrm{integralSum} f vol)\bigr)$$$

Lean4

theorem integrable_iff_cauchy [CompleteSpace F] :
    Integrable I l f vol ↔ Cauchy ((l.toFilteriUnion I ⊤).map (integralSum f vol)) :=
  cauchy_map_iff_exists_tendsto.symm

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