to_subbox — Mathlib

English

If h is Integrable on I, then for some J ≤ I and y with HasIntegral J, the map toFilteriUnion yields a Tendsto to y.

Русский

Если h интегрируем на I, то найдётся J ≤ I и y, для которых HasIntegral J, и отображение к toFilteriUnion сходится к y.

LaTeX

$$$\exists y,\ HasIntegral J l f vol y \land \ Tendsto (\text{integralSum } f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (\mathcal{NHDS} y)$$$

Lean4

/-- If `f` is integrable on a box `I`, then it is integrable on any subbox of `I`. -/
theorem to_subbox (h : Integrable I l f vol) (hJ : J ≤ I) : Integrable J l f vol :=
  (h.to_subbox_aux hJ).imp fun _ => And.left

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