aecover_Ioi_of_Ioi — Mathlib

English

Let A be a reference point and a_i → A with respect to l; then the family Ioi(a_i) covers μ on the tail above A in the sense of AE-cover with respect to l.

Русский

Пусть A — опорная точка, и a_i сходится к A по l; тогда семейство Ioi(a_i) покрывает μ на хвосте над A в смысле AE-покрытия по отношению к l.

LaTeX

$$$\\mathrm{AECover}(\\mu, l)(i \\mapsto \\mathrm{Ioi}(a_i)).$$$

Lean4

theorem aecover_Ioi_of_Ioi : AECover (μ.restrict (Ioi A)) l fun i ↦ Ioi (a i)
    where
  ae_eventually_mem := (ae_restrict_mem measurableSet_Ioi).mono fun _x hx ↦ ha.eventually <| eventually_lt_nhds hx
  measurableSet _ := measurableSet_Ioi

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