aecover_Ico_of_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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