SingletonDetourNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The existing small physical disk construction supplies actual quotient neighborhoods with path connected boundaries avoiding the whole obstacle. These are the neighborhoods used in finite detours.

theorem OAI.CircleDomainRigidity.exists_singleton_detour_neighborhood line 18