OAI/Combinatorics/EditDistance/Slots.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Position-tagged concatenation and repeated slots

  1. def OAI.EditSlots.project line 14
  2. lemma OAI.EditSlots.project_map line 16
  3. def OAI.EditSlots.tagged line 20
  4. lemma OAI.EditSlots.project_tagged line 23
  5. lemma OAI.EditSlots.project_length_partition line 37
  6. lemma OAI.EditSlots.tagged_length line 50
  7. theorem OAI.EditSlots.sum_indel_le_tagged line 56
  8. lemma OAI.EditSlots.cost_tagged_le line 96
  9. def OAI.EditSlots.fixedFn line 107
  10. lemma OAI.EditSlots.ofFn_fixedFn line 110
  11. abbrev OAI.EditSlots.Slots line 118
  12. def OAI.EditSlots.component line 120
  13. lemma OAI.EditSlots.slots_card line 124
  14. def OAI.EditSlots.enumeration line 130
  15. lemma OAI.EditSlots.enumeration_nodup line 133
  16. lemma OAI.EditSlots.enumeration_full line 136
  17. lemma OAI.EditSlots.sum_slots line 140
  18. def OAI.EditSlots.multiplicity line 145
  19. lemma OAI.EditSlots.sum_slots_delta line 147
  20. lemma OAI.EditSlots.sum_multiplicity line 166