aecover_Ioc_of_Ioo — Mathlib

English

If a(i) → A and b(i) → B, then the family Ioo(a(i), b(i)) covers μ almost everywhere on Ico(A, B).

Русский

Если a(i) → A и b(i) → B, то семейство Ioo(a(i), b(i)) покрывает μ почти всюду на Ico(A, B).

LaTeX

$$$\text{Tendsto } a\, l\,(\nhds A) \land \text{Tendsto } b\, l\,(\nhds B) \Rightarrow \mathrm{AECover}(\mu\restriction \mathrm{Ioo}\, A B, l, i \mapsto \mathrm{Ioo}(a(i), b(i))).$$$

Lean4

theorem aecover_Ioc_of_Ioo (ha : Tendsto a l (𝓝 A)) (hb : Tendsto b l (𝓝 B)) :
    AECover (μ.restrict <| Ioc A B) l fun i => Ioo (a i) (b i) :=
  (aecover_Ioo_of_Ioo ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Ioc).ge

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