eventually — Mathlib

English

If f is integrable at l, then for every set in l.smallSets, f is integrable on that set.

Русский

Если f интегрируемо на л, то на любом малом множестве в l.smallSets f интегрируема.

LaTeX

$$$\\exists s \\in l.smallSets,\\ \\operatorname{IntegrableOn}(f, s, \\mu)$$$

Lean4

protected theorem eventually (h : IntegrableAtFilter f l μ) : ∀ᶠ s in l.smallSets, IntegrableOn f s μ :=
  Iff.mpr (eventually_smallSets' fun _s _t hst ht => ht.mono_set hst) h

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