OAI/Analysis/CircleDomains/Topology/TerminalSimpleArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Erase loops in the terminal portion after the last collar hit. The resulting arc meets the collar only at its initial endpoint.

  1. theorem OAI.CircleDomainRigidity.exists_terminal_simple_arc line 18