OAI/Combinatorics/TreeEdit/CyclicWords.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.Words.get line 15
  2. def OAI.TreeEdit.Words.ofFn line 17
  3. lemma OAI.TreeEdit.Words.at_ofFn line 19
  4. def OAI.TreeEdit.Words.map line 22
  5. lemma OAI.TreeEdit.Words.at_map line 25
  6. lemma OAI.TreeEdit.Words.ext line 28
  7. def OAI.TreeEdit.Words.cycles line 35
  8. lemma OAI.TreeEdit.Words.at_cycles line 39
  9. lemma OAI.TreeEdit.Words.cycle_coordinates line 45
  10. lemma OAI.TreeEdit.Words.cycle_offset_strict line 53
  11. lemma OAI.TreeEdit.Words.cycle_block_alignment line 63
  12. lemma OAI.TreeEdit.Words.cycle_fiber_bound line 98
  13. lemma OAI.TreeEdit.Words.cycles_deficit line 121
  14. lemma OAI.TreeEdit.lcs_map_of_injective line 160
  15. lemma OAI.TreeEdit.deficit_singleton line 175
  16. lemma OAI.TreeEdit.translation_cycle line 185