English
Let α be a linear ordered space with NoMinOrder, and let l be a filter on ι. If a: ι → α tends to the bottom with respect to l and b: ι → α tends to the top with respect to l, then the family of half-open intervals Ioc(a(i), b(i)) forms an almost-everywhere cover of μ with respect to l; i.e., almost every x lies in some Ioc(a(i), b(i)) as i varies along l.
Русский
Пусть α — линейно упорядчённое множество с условием NoMinOrder, пусть l — фильтр на ι. Если a: ι → α стремится к нижней границе по l, а b: ι → α — к верхней по l, то семейство полузакрытых интервалов Ioc(a(i), b(i)) образует почти повседневное покрытие μ относительно l; т.е. почти каждая точка x принадлежит некоторому Ioc(a(i), b(i)) при переборе i вдоль l.
LaTeX
$$$\text{Tendsto } a\, l\, (\text{atBot}) \land \text{Tendsto } b\, l\, (\text{atTop}) \Rightarrow \mathrm{AECover}(\mu, l, i \mapsto Ioc(a(i), b(i))).$$$
Lean4
theorem aecover_Ioc [NoMinOrder α] : AECover μ l fun i => Ioc (a i) (b i) :=
(aecover_Ioi ha).inter (aecover_Iic hb)
