OAI/Combinatorics/FiniteCircle/TaggedRows.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.taggedRow line 9
  2. theorem OAI.FiniteCircle.taggedRow_nil line 12
  3. theorem OAI.FiniteCircle.taggedRow_cons line 13
  4. theorem OAI.FiniteCircle.filter_map_tag line 16
  5. theorem OAI.FiniteCircle.filter_taggedRow line 24
  6. theorem OAI.FiniteCircle.sum_filter_tag_length line 38
  7. theorem OAI.FiniteCircle.length_taggedRow line 51
  8. theorem OAI.FiniteCircle.lcs_taggedRow_le line 59
  9. theorem OAI.FiniteCircle.get_segment line 74
  10. def OAI.FiniteCircle.WordMatching.onSegments line 86
  11. theorem OAI.FiniteCircle.WordMatching.card_onSegments_le line 131
  12. theorem OAI.FiniteCircle.position_decomposition line 140
  13. theorem OAI.FiniteCircle.split_positions_gap line 147
  14. def OAI.FiniteCircle.WordMatching.singleTargetRow line 172
  15. theorem OAI.FiniteCircle.WordMatching.spanLoss_of_split line 175
  16. theorem OAI.FiniteCircle.WordMatching.sourceLoss_of_single line 221
  17. theorem OAI.FiniteCircle.row_separation line 253
  18. theorem OAI.FiniteCircle.length_flatMap_uniform line 296
  19. theorem OAI.FiniteCircle.segment_flatMap_uniform line 305
  20. theorem OAI.FiniteCircle.get_flatMap_uniform line 321
  21. theorem OAI.FiniteCircle.tag_get_taggedRow line 351
  22. theorem OAI.FiniteCircle.tag_get_rows line 363