OAI/Analysis/CircleDomains/Topology/FinalCollarPrescribedLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The final collar, oriented from the limiting endpoint inward, uses the prescribed common limits of actual last-entry fragments.

  1. theorem OAI.CircleDomainRigidity.exists_final_collar_path_of_limits line 24