aecover_Ico — Mathlib

English

If α has no maximum, and a_i → atBot and b_i → atTop along l, then the family Ico(a_i, b_i) forms an AE-cover of μ with respect to l.

Русский

Если у пространства α отсутствует максимальный элемент, и a_i сходится к нижней границе, а b_i к верхней вдоль фильтра l, то семейство интервалов Ico(a_i, b_i) образует AE-покрытие меры μ по отношению к l.

LaTeX

$$$[NoMaxOrder\\;\\alpha]\\Rightarrow \\mathrm{AECover}(\\mu, l)(i \\mapsto \\mathrm{Ico}(a_i, b_i)).$$$

Lean4

theorem aecover_Ico [NoMaxOrder α] : AECover μ l fun i => Ico (a i) (b i) :=
  (aecover_Ici ha).inter (aecover_Iio hb)

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