OAI/Analysis/MarkovType/WordAction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.wordMap line 10
  2. theorem OAI.MarkovSuperreflexivity.wordMap_nil line 14
  3. theorem OAI.MarkovSuperreflexivity.wordMap_nil_apply line 16
  4. theorem OAI.MarkovSuperreflexivity.wordMap_nil_symm line 18
  5. theorem OAI.MarkovSuperreflexivity.wordMap_cons line 20
  6. theorem OAI.MarkovSuperreflexivity.wordMap_cons_symm line 23
  7. theorem OAI.MarkovSuperreflexivity.wordMap_singleton line 27
  8. theorem OAI.MarkovSuperreflexivity.wordMap_append line 30
  9. theorem OAI.MarkovSuperreflexivity.wordMap_append_equiv line 36
  10. theorem OAI.MarkovSuperreflexivity.wordMap_append_symm line 42
  11. def OAI.MarkovSuperreflexivity.inverseWord line 47
  12. theorem OAI.MarkovSuperreflexivity.inverseWord_nil line 49
  13. theorem OAI.MarkovSuperreflexivity.inverseWord_cons line 51
  14. theorem OAI.MarkovSuperreflexivity.inverseWord_length line 55
  15. theorem OAI.MarkovSuperreflexivity.wordMap_inverseWord line 59
  16. theorem OAI.MarkovSuperreflexivity.wordMap_cancel line 69
  17. theorem OAI.MarkovSuperreflexivity.wordMap_reduceWord line 76
  18. theorem OAI.MarkovSuperreflexivity.wordMap_add_int line 80
  19. theorem OAI.MarkovSuperreflexivity.wordMap_symm_add_int line 87
  20. theorem OAI.MarkovSuperreflexivity.prefixState_wordMap line 92
  21. theorem OAI.MarkovSuperreflexivity.prefixState_int line 98
  22. theorem OAI.MarkovSuperreflexivity.prefixState_wordMap_add_int line 104
  23. theorem OAI.MarkovSuperreflexivity.wordMap_displacement_le line 109
  24. theorem OAI.MarkovSuperreflexivity.wordMap_displacement_lt line 120
  25. theorem OAI.MarkovSuperreflexivity.wordMap_symm_displacement_le line 131