OAI/Analysis/CoulombTransport/CompactSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.exists_uniform_compact_separation line 14

   Source documentation

   Finitely many pairwise disjoint compact components in a metric space have one positive separation bound. Empty components and an empty index type are allowed, so no auxiliary nonemptiness assumptions are needed.

   theorem exists_uniform_compact_separation {α : Type uAlpha} {ι : Type uIndex} [MetricSpace α] [Finite ι]
       (K : ι → Set α) (hcompact : ∀ i, IsCompact (K i))
       (hdisjoint : Pairwise (fun i j => Disjoint (K i) (K j))) :
       ∃ eta : ℝ, 0 < eta ∧
         ∀ i j, i ≠ j → ∀ x ∈ K i, ∀ y ∈ K j, eta ≤ dist x y := by
   …