OAI/Analysis/CircleDomains/Selection/LinkedFragmentSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous selection of actual fragments and joining arcs. Both ends of each chosen fragment lie in the neighborhoods needed by its two neighbors.

  1. theorem OAI.CircleDomainRigidity.exists_linked_fragment_selection line 20