Positive separation of disjoint nonempty compact sets
ProvedPositiveSeparationcrossing-consequencesgeometrypolygonal
If and are nonempty, disjoint compact subsets of the Euclidean plane, then they have positive mutual separation:
\exists \delta>0,\quad orall a\in A\ orall b\in B,\quad \delta\le d(a,b).This is the compactness lemma that turns disjointness of the old prefix region and the polygonal tail into a uniform distance bound.
Preamble
import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Topology.Order.Compact open Classical noncomputable section
Formal statement
lemma PositiveSeparation {A B : Set (EuclideanSpace ℝ (Fin 2))}
(hA : A.Nonempty) (hB : B.Nonempty) (hAc : IsCompact A) (hBc : IsCompact B)
(hdisj : Disjoint A B) :
∃ δ : ℝ, 0 < δ ∧ ∀ a, a ∈ A → ∀ b, b ∈ B → δ ≤ dist a b := by sorrySource