Small closed balls around finitely many points are separated

Around finitely many points of a metric space, closed balls of a small enough common radius lie in prescribed neighbourhoods of their centres and are pairwise far apart: the radius is less than half the distance between any two distinct centres, so the balls are disjoint and no point of one ball lies on the boundary sphere of another. This is the geometric input for splitting a sum over points near the centres as a sum over the balls, as in the contour-integral computation of sums over the roots of a polynomial.

Main declarations

• TauCeti.exists_pos_closedBall_subset_and_lt_dist: a common radius that is small enough for every centre at once.
• TauCeti.eq_of_dist_lt_of_dist_lt: two such centres within the radius of a common point coincide.

theorem TauCeti.exists_pos_closedBall_subset_and_lt_dist {X : Type u_1} [MetricSpace X] {T : Finset X} {U : X → Set X} (hU : ∀ w ∈ T, U w ∈ nhds w) : ∃ r > 0, (∀ w ∈ T, Metric.closedBall w r ⊆ U w) ∧ ∀ w ∈ T, ∀ w' ∈ T, w ≠ w' → 2 * r < dist w w'

Around finitely many points, closed balls of a small enough common radius lie in prescribed neighbourhoods of their centres and are pairwise far apart: twice the radius is less than the distance between any two distinct centres.

theorem TauCeti.eq_of_dist_lt_of_dist_lt {Y : Type u_2} [PseudoMetricSpace Y] {w w' y : Y} {r : ℝ} (hsep : w ≠ w' → 2 * r < dist w w') (h : dist y w < r) (h' : dist y w' < r) : w = w'

Two points that are either equal or more than 2 * r apart are equal if both lie within r of a common point.