aecover_Iio_of_Iic — Mathlib

English

If b_i → B, then μ restricted to Iio(B) is AE-covered by Iio(b_i) with respect to l.

Русский

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

LaTeX

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

Lean4

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

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