English
In a linearly ordered topological space with no minimum or maximum, if the two nets a_i and b_i tend to the bottom and the top along a filter l, then the family of open intervals Ioo(a_i, b_i) forms an almost-everywhere cover (AE-cover) of the measure μ with respect to l.
Русский
В линейно упорядоченном топологическом пространстве без минимального и максимального элемента, если две сетки a_i и b_i стремятся к нижней и верхней границе вдоль фильтра l, тогда семейство интервалов Ioo(a_i, b_i) образует AE-покрытие меры μ по отношению к l.
LaTeX
$$$([NoMinOrder\\;\\alpha]\\ [NoMaxOrder\\;\\alpha] \\wedge \\mathrm{Tendsto}\\ a\\ l\\ atBot\\wedge \\mathrm{Tendsto}\\ b\\ l\\ atTop)\\Rightarrow \\mathrm{AECover}(\\mu, l)(i \\mapsto \\mathrm{Ioo}(a_i, b_i)).$$
Lean4
theorem aecover_Ioo [NoMinOrder α] [NoMaxOrder α] : AECover μ l fun i => Ioo (a i) (b i) :=
(aecover_Ioi ha).inter (aecover_Iio hb)
