Common Thickening Radius For Finitely Many Compact Sets

This is a metric separation lemma for finitely many pairwise disjoint compact sets.

Let $X$ be a metric space, let $N\in\mathbb N$, and let $K_i\subseteq X$ be compact for every $i\in\mathbb N$. Assume that distinct sets are pairwise disjoint:

Then there exists a radius $\rho>0$ such that for all distinct $i,j<N$, the metric thickenings are disjoint:

The Lean declaration is exists_thickening_pairwise_disjoint_readable. Only the first $N$ indices are required to have disjoint thickenings; the conclusion makes no assertion about indices at or beyond $N$.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy. Shown in its original module context. Proof omitted.

theorem exists_thickening_pairwise_disjoint (N : ℕ) (Kc : ℕ → Set X)
    (hcomp : ∀ n, IsCompact (Kc n)) (hdisj : ∀ i j, i ≠ j → Disjoint (Kc i) (Kc j)) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ i < N, ∀ j < N, i ≠ j →
      Disjoint (Metric.thickening ρ (Kc i)) (Metric.thickening ρ (Kc j))

Module navigation

Module: Energy/Euclidean/Slope/Density.

Previous: lowerSemicontinuous_secant · Next: exists_patch_of_isCompact.

Source excerpt, lines 123–126 · Frozen source 408915f.