OAI/Combinatorics/FiniteCircle/Matching.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.segment line 9
  2. theorem OAI.FiniteCircle.segment_sublist line 11
  3. theorem OAI.FiniteCircle.length_segment line 14
  4. theorem OAI.FiniteCircle.unequalDeficit_segment_sublist_le line 19
  5. theorem OAI.FiniteCircle.unequalDeficit_symm line 27
  6. inductive OAI.FiniteCircle.Slide line 31
  7. theorem OAI.FiniteCircle.Slide.symm line 40
  8. theorem OAI.FiniteCircle.Slide.length_eq line 45
  9. theorem OAI.FiniteCircle.Slide.append_left line 48
  10. theorem OAI.FiniteCircle.Slide.append_right line 53
  11. theorem OAI.FiniteCircle.Slide.common_delete line 60
  12. theorem OAI.FiniteCircle.Slide.segment_deficit_le_two line 73
  13. inductive OAI.FiniteCircle.SlidePath line 82
  14. theorem OAI.FiniteCircle.SlidePath.trans line 89
  15. theorem OAI.FiniteCircle.SlidePath.symm line 94
  16. theorem OAI.FiniteCircle.SlidePath.append_left line 99
  17. theorem OAI.FiniteCircle.SlidePath.append_right line 104
  18. theorem OAI.FiniteCircle.SlidePath.length_eq line 109
  19. theorem OAI.FiniteCircle.SlidePath.to_padded_sublist line 114
  20. theorem OAI.FiniteCircle.exists_slidePath line 130
  21. structure OAI.FiniteCircle.WordMatching line 139
  22. theorem OAI.FiniteCircle.WordMatching.le_lcs line 147
  23. def OAI.FiniteCircle.WordMatching.restrict line 166
  24. def OAI.FiniteCircle.WordMatching.symm line 171
  25. def OAI.FiniteCircle.WordMatching.rightSpan line 176
  26. theorem OAI.FiniteCircle.WordMatching.rightSpan_matched_iff line 179
  27. theorem OAI.FiniteCircle.WordMatching.rightSpan_disjoint line 189
  28. theorem OAI.FiniteCircle.WordMatching.sum_span_card_le line 198
  29. theorem OAI.FiniteCircle.exists_lcs_matching line 213
  30. def OAI.FiniteCircle.WordMatching.sourceBlock line 224
  31. theorem OAI.FiniteCircle.WordMatching.mem_sourceBlock line 227
  32. theorem OAI.FiniteCircle.WordMatching.sourceBlock_card_le line 230
  33. theorem OAI.FiniteCircle.WordMatching.sum_sourceBlock_card line 248
  34. theorem OAI.FiniteCircle.WordMatching.sourceBlock_order line 260
  35. theorem OAI.FiniteCircle.WordMatching.sourceBlock_convex line 268
  36. theorem OAI.FiniteCircle.WordMatching.card_le_rightSpan line 277
  37. def OAI.FiniteCircle.WordMatching.sourceLoss line 286
  38. def OAI.FiniteCircle.WordMatching.spanLoss line 288
  39. theorem OAI.FiniteCircle.WordMatching.sum_sourceLoss line 291
  40. theorem OAI.FiniteCircle.WordMatching.sum_spanLoss_le line 300
  41. def OAI.FiniteCircle.WordMatching.ConvexIndices line 317
  42. theorem OAI.FiniteCircle.WordMatching.rightSpan_mono line 320
  43. theorem OAI.FiniteCircle.WordMatching.rightSpan_eq_Icc line 326
  44. theorem OAI.FiniteCircle.WordMatching.convex_eq_Icc line 337
  45. theorem OAI.FiniteCircle.WordMatching.card_span_unmatched line 347
  46. theorem OAI.FiniteCircle.WordMatching.span_holes_mono line 366
  47. theorem OAI.FiniteCircle.WordMatching.leftSpan_sourceBlock_card_le line 372
  48. theorem OAI.FiniteCircle.WordMatching.left_span_holes_le_sourceLoss line 395
  49. theorem OAI.FiniteCircle.WordMatching.right_span_holes_le_spanLoss line 401