OAI/Analysis/CircleDomains/Topology/OneEndedCollarSplicing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Attach one actual retained prefix to the final collar tail, keeping its original initial point and using the joint prefix/tail budget.

  1. theorem OAI.CircleDomainRigidity.exists_oneEnded_collar_splicing_of_limits line 20