aecover_Ioo_of_Ioo — Mathlib

English

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

Русский

Если a_i стремится к A, а b_i к B, то интервалы Ioo(a_i, b_i) AE-покрывают интервал Ioo(A, B) по мере μ и вдоль l.

LaTeX

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

Lean4

theorem aecover_Ioo_of_Ioo : AECover (μ.restrict <| Ioo A B) l fun i => Ioo (a i) (b i) :=
  ((aecover_Ioi_of_Ioi ha).mono <| Measure.restrict_mono Ioo_subset_Ioi_self le_rfl).inter
    ((aecover_Iio_of_Iio hb).mono <| Measure.restrict_mono Ioo_subset_Iio_self le_rfl)

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