aecover_closedBall — Mathlib

English

If r_i tends to infinity along l, then the family of closed balls B_i = closedBall(x, r_i) forms an AECover.

Русский

Если r_i растет по ленте l, семейство замкнутых шаров образует AECover.

LaTeX

$$$\\text{AECover } μ l (i \\mapsto \\text{closedBall }(x, r_i))$$$

Lean4

theorem aecover_closedBall {x : α} {r : ι → ℝ} (hr : Tendsto r l atTop) :
    AECover μ l (fun i ↦ Metric.closedBall x (r i))
    where
  measurableSet _ := Metric.isClosed_closedBall.measurableSet
  ae_eventually_mem := by
    filter_upwards with y
    filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

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