aecover_Ioo_of_Icc — Mathlib

English

If a_i → A and b_i → B, then the closed intervals Icc(a_i, b_i) form an AE-cover of the closed interval Icc(A,B).

Русский

Если a_i сходится к A и b_i — к B, то Icc(a_i, b_i) образуют AE-покрытие Icc(A,B).

LaTeX

$$$\\mathrm{AECover}(\\mu\\restriction \\mathrm{Ioo}(A, B), l)(i \\mapsto \\mathrm{Icc}(a_i, b_i)).$$$

Lean4

theorem aecover_Ioo_of_Icc : AECover (μ.restrict <| Ioo A B) l fun i => Icc (a i) (b i) :=
  (aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Icc_self) fun _ ↦ measurableSet_Icc

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