aecover_Ico_of_Ico — Mathlib

English

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

Русский

Если a(i) → A и b(i) → B, то семейство Ico(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{Ico}\, A B, l, i \mapsto \mathrm{Ico}(a(i), b(i))).$$$

Lean4

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

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