aecover_Ioo_of_Ico — Mathlib

English

If a_i → A and b_i → B, then the half-open intervals Ico(a_i, b_i) AE-cover the half-open interval Ioo(A,B) with respect to μ and l.

Русский

Если a_i сходится к A, а b_i к B, то Ico(a_i, b_i) AE-покрывают Ioo(A,B).

LaTeX

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

Lean4

theorem aecover_Ioo_of_Ico : AECover (μ.restrict <| Ioo A B) l fun i => Ico (a i) (b i) :=
  (aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Ico_self) fun _ ↦ measurableSet_Ico

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