OAI/Analysis/CircleDomains/Selection/FragmentReindexing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A cofinal reindexing preserves each fixed actual fragment eventually; only the deliberately unused early triangular entries can differ.

  1. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_reindex_eventually line 18
  2. theorem OAI.CircleDomainRigidity.lastEntryFragmentArray_reindex_eventually line 30