OAI/Analysis/MarkovType/PeriodicArcs.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.periodicIco line 11
  2. def OAI.MarkovSuperreflexivity.periodicIcc line 13
  3. def OAI.MarkovSuperreflexivity.periodicIoo line 15
  4. theorem OAI.MarkovSuperreflexivity.mem_periodicIco_iff line 17
  5. theorem OAI.MarkovSuperreflexivity.mem_periodicIcc_iff line 32
  6. theorem OAI.MarkovSuperreflexivity.not_mem_periodicIco_iff line 47
  7. theorem OAI.MarkovSuperreflexivity.not_mem_periodicIcc_iff line 63
  8. def OAI.MarkovSuperreflexivity.arcRank line 79
  9. def OAI.MarkovSuperreflexivity.alpha line 81
  10. def OAI.MarkovSuperreflexivity.beta line 83
  11. def OAI.MarkovSuperreflexivity.arc line 85
  12. def OAI.MarkovSuperreflexivity.openArc line 87
  13. def OAI.MarkovSuperreflexivity.closedArc line 89
  14. theorem OAI.MarkovSuperreflexivity.alpha_pos line 91
  15. theorem OAI.MarkovSuperreflexivity.alpha_lt_beta line 95
  16. theorem OAI.MarkovSuperreflexivity.beta_lt_one line 99
  17. theorem OAI.MarkovSuperreflexivity.beta_lt_alpha_add_one line 103
  18. theorem OAI.MarkovSuperreflexivity.beta_lt_alpha_or line 107
  19. theorem OAI.MarkovSuperreflexivity.openArc_subset_arc line 115
  20. theorem OAI.MarkovSuperreflexivity.arc_subset_closedArc line 119
  21. theorem OAI.MarkovSuperreflexivity.closedArc_fract line 123
  22. theorem OAI.MarkovSuperreflexivity.not_mem_closedArc_int line 135
  23. theorem OAI.MarkovSuperreflexivity.not_mem_arc_int line 141
  24. theorem OAI.MarkovSuperreflexivity.disjoint_closedArc line 145
  25. theorem OAI.MarkovSuperreflexivity.disjoint_arc line 153
  26. theorem OAI.MarkovSuperreflexivity.mem_arc_add_int_iff line 159
  27. theorem OAI.MarkovSuperreflexivity.mem_openArc_add_int_iff line 167
  28. theorem OAI.MarkovSuperreflexivity.isOpen_openArc line 175
  29. theorem OAI.MarkovSuperreflexivity.openArc_subset_interior_arc line 182
  30. def OAI.MarkovSuperreflexivity.positiveOrderIso line 185
  31. def OAI.MarkovSuperreflexivity.letterOrderIso line 188
  32. def OAI.MarkovSuperreflexivity.letterHomeomorph line 191
  33. theorem OAI.MarkovSuperreflexivity.letterHomeomorph_apply line 193
  34. theorem OAI.MarkovSuperreflexivity.letterOrderIso_inv line 196
  35. theorem OAI.MarkovSuperreflexivity.letterOrderIso_add_int line 200
  36. theorem OAI.MarkovSuperreflexivity.positiveOrderIso_start line 207
  37. theorem OAI.MarkovSuperreflexivity.positiveOrderIso_break line 211
  38. theorem OAI.MarkovSuperreflexivity.positiveOrderIso_end line 219
  39. def OAI.MarkovSuperreflexivity.letterPeriodShift line 225
  40. theorem OAI.MarkovSuperreflexivity.letterOrderIso_beta_inv_base line 227
  41. theorem OAI.MarkovSuperreflexivity.letterOrderIso_alpha_inv_add_one_base line 239
  42. theorem OAI.MarkovSuperreflexivity.letterOrderIso_beta_inv line 257
  43. theorem OAI.MarkovSuperreflexivity.letterOrderIso_alpha_inv_add_one line 263
  44. theorem OAI.MarkovSuperreflexivity.mem_arc_iff_not_mem_inv_arc line 270
  45. theorem OAI.MarkovSuperreflexivity.image_compl_arc line 290
  46. theorem OAI.MarkovSuperreflexivity.symm_mem_inv_arc_iff line 300
  47. theorem OAI.MarkovSuperreflexivity.map_mem_openArc_of_not_mem_closedArc line 311
  48. theorem OAI.MarkovSuperreflexivity.letterOrderIso_zero_mem_openArc line 319
  49. theorem OAI.MarkovSuperreflexivity.letterOrderIso_mem_openArc_of_mem_openArc line 323
  50. theorem OAI.MarkovSuperreflexivity.positiveOrderIso_displacement line 330
  51. theorem OAI.MarkovSuperreflexivity.letterOrderIso_abs_move_le line 344
  52. theorem OAI.MarkovSuperreflexivity.letterOrderIso_displacement_lt line 356