English
Definition: interUnionBalls(xs,u,V) collects points that lie in a V(n)-ball around some xs(m) with m ≤ u(n), for every n.
Русский
Определение: interUnionBalls(xs,u,V) собирает точки, лежащие внутри V(n)-шара вокруг некоторого xs(m) с m ≤ u(n) для каждого n.
LaTeX
$$$\\operatorname{interUnionBalls}(xs,u,V) \;:=\\; \\bigcap_{n} \\bigcup_{m \\le u(n)} \\operatorname{ball}(xs(m), (\\operatorname{Prod.swap}^{-1}' V(n)))$$$
Lean4
/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
Designed to be relatively compact when `V n` tends to the diagonal. -/
def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
