aecover_ball — Mathlib

English

There exists a family of balls B_i = Ball(x, r_i) forming an AECover provided r_i → ∞ along l.

Русский

Существуют шары B_i = Ball(x, r_i), образующие AECover, если r_i простираются вверх по l.

LaTeX

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

Lean4

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

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