OAI/Analysis/CircleDomains/Topology/LocalizedCollarSplicing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The collar endpoint may be selected in any prescribed neighborhood of its limiting outer hit point, for attaching a common middle fragment.

  1. theorem OAI.CircleDomainRigidity.exists_collar_path_from_fragment_limits_near line 19