aecover_Icc_of_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem aecover_Icc_of_Ioc (ha : Tendsto a l (𝓝 A)) (hb : Tendsto b l (𝓝 B)) :
    AECover (μ.restrict <| Icc A B) l fun i => Ioc (a i) (b i) :=
  (aecover_Ioo_of_Ioc ha hb).mono (Measure.restrict_congr_set Ioo_ae_eq_Icc).ge

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