aecover_Ioo_of_Ioc — Mathlib

English

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

Русский

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

Lean4

theorem aecover_Ioo_of_Ioc : AECover (μ.restrict <| Ioo A B) l fun i => Ioc (a i) (b i) :=
  (aecover_Ioo_of_Ioo ha hb).superset (fun _ ↦ Ioo_subset_Ioc_self) fun _ ↦ measurableSet_Ioc

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