OAI/Combinatorics/EditDistance/AlphabetSupremum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Alphabet equivalences and universe-independent suprema

  1. lemma OAI.EditDistortion.E_le_of_alphabet_embedding line 12
  2. lemma OAI.EditDistortion.E_equiv line 37
  3. theorem OAI.EditDistortion.alphabet_values_eq_all line 42
  4. theorem OAI.EditDistortion.alphabetSup_eq_all line 57