OAI/Combinatorics/EditDistance/WholeMaps.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous whole-domain maps and fixed-length binary upper bounds

  1. lemma OAI.EditUpper.coarse_whole_map line 14
  2. theorem OAI.EditUpper.eventual_whole_maps line 43
  3. theorem OAI.EditUpper.whole_maps_all_lengths line 75
  4. theorem OAI.EditUpper.fixed_length_binary_upper line 119