aecover_Ioi_of_Ici — Mathlib

English

For any sequence a_i tending to A, the sets Ici(a_i) cover μ restricted to Ioi(A) in the AE sense with respect to l.

Русский

Для любой последовательности a_i, стремящейся к A, множества Ici(a_i) покрывают μ, ограниченную до Ioi(A), в смысле AE-покрытия относительно l.

LaTeX

$$$\\mathrm{AECover}(\\mu\\restriction \\mathrm{Ioi}(A), l)(i \\mapsto \\mathrm{Ici}(a_i)).$$$

Lean4

theorem aecover_Ioi_of_Ici : AECover (μ.restrict (Ioi A)) l fun i ↦ Ici (a i) :=
  (aecover_Ioi_of_Ioi ha).superset (fun _ ↦ Ioi_subset_Ici_self) fun _ ↦ measurableSet_Ici

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