hasIntegral — Mathlib

English

If f is Integrable on I with l and vol, then there exists y such that HasIntegral I l f vol y holds, i.e., the integral exists as a limit.

Русский

Если функция интегрируема, существует y, для которого выполняется HasIntegral; интеграл существует как предел.

LaTeX

$$$\mathrm{Integrable}(I,l,f,vol) \Rightarrow \exists y\; \mathrm{HasIntegral}(I,l,f,vol,y)$$$

Lean4

protected theorem hasIntegral (h : Integrable I l f vol) : HasIntegral I l f vol (integral I l f vol) :=
  by
  rw [integral, dif_pos h]
  exact Classical.choose_spec h

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