SmallCollarArcs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small image neighborhoods on a finite-cost simple collar admit actual joining arcs of arbitrarily small cost. Compactness converts parameter neighborhoods into neighborhoods in the ambient space.

theorem OAI.CircleDomainRigidity.exists_small_collar_arcs line 18