tendsto — Mathlib

English

From HasIntegral we obtain Tendsto of integralSum to y along the specified filter.

Русский

Из HasIntegral следует, что integralSum стремится к y вдоль заданного фильтра.

LaTeX

$$$\mathrm{HasIntegral}(I, l, f, vol, y) \Rightarrow \mathrm{Tendsto}(\mathrm{integralSum} f vol) (l.toFilteriUnion I \top) (\mathcal{N} y)$$$

Lean4

/-- Reinterpret `BoxIntegral.HasIntegral` as `Filter.Tendsto`, e.g., dot-notation theorems
that are shadowed in the `BoxIntegral.HasIntegral` namespace. -/
theorem tendsto (h : HasIntegral I l f vol y) : Tendsto (integralSum f vol) (l.toFilteriUnion I ⊤) (𝓝 y) :=
  h

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