OAI/Combinatorics/FiniteCircle/BlockMatching.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.get_encode_block line 11
  2. theorem OAI.FiniteCircle.get_encode line 33
  3. theorem OAI.FiniteCircle.indexSpan_ofFn line 47
  4. def OAI.FiniteCircle.WordMatching.localIndices line 62
  5. theorem OAI.FiniteCircle.WordMatching.localIndices_length line 67
  6. theorem OAI.FiniteCircle.WordMatching.mod_strictMono_on_block line 70
  7. theorem OAI.FiniteCircle.WordMatching.localIndices_sorted line 80
  8. theorem OAI.FiniteCircle.WordMatching.localIndices_span line 88
  9. def OAI.FiniteCircle.WordMatching.blockPair line 107
  10. theorem OAI.FiniteCircle.WordMatching.blockPair_convex line 110
  11. def OAI.FiniteCircle.WordMatching.targetBlocks line 117
  12. theorem OAI.FiniteCircle.WordMatching.targetBlocks_card_le_three line 120
  13. theorem OAI.FiniteCircle.WordMatching.sum_blockPair_card line 154
  14. theorem OAI.FiniteCircle.WordMatching.exists_large_blockPair line 167