OAI/Analysis/CircleDomains/Topology/InitialCollarPrescribedLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Initial collar splicing on a prescribed common subsequence and budget. This retains the shared budget with the final tail and middle fragment.

  1. theorem OAI.CircleDomainRigidity.exists_initial_collar_path_of_limits line 21