aecover_Iio_of_Iio — Mathlib

English

If b_i → B from below along l, then the sets Iio(b_i) form an AE-cover of μ restricted to Iio(B).

Русский

Если b_i сходится к B снизу вдоль l, то множества Iio(b_i) образуют AE-покрытие μ, ограниченной до Iio(B).

LaTeX

$$$\\mathrm{AECover}(\\mu\\restriction \\mathrm{Iio}(B), l)(i \\mapsto \\mathrm{Iio}(b_i)).$$$

Lean4

theorem aecover_Iio_of_Iio : AECover (μ.restrict (Iio B)) l fun i ↦ Iio (b i) :=
  aecover_Ioi_of_Ioi (α := αᵒᵈ) hb

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