OAI/Analysis/MarkovType/OrderedSequences.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.C00 line 12
  2. def OAI.MarkovSuperreflexivity.C00.basis line 16
  3. def OAI.MarkovSuperreflexivity.C00.place line 18
  4. def OAI.MarkovSuperreflexivity.C00.ofArray line 21
  5. def OAI.MarkovSuperreflexivity.C00.placeLinear line 23
  6. def OAI.MarkovSuperreflexivity.C00.arrayLinear line 30
  7. theorem OAI.MarkovSuperreflexivity.C00.placeLinear_apply line 32
  8. theorem OAI.MarkovSuperreflexivity.C00.arrayLinear_apply line 35
  9. theorem OAI.MarkovSuperreflexivity.C00.ofArray_apply line 38
  10. theorem OAI.MarkovSuperreflexivity.C00.ofArray_injective line 49
  11. def OAI.MarkovSuperreflexivity.C00.mergeIndex line 54
  12. def OAI.MarkovSuperreflexivity.C00.mergeAt line 56
  13. theorem OAI.MarkovSuperreflexivity.C00.mergeAt_zero line 58
  14. theorem OAI.MarkovSuperreflexivity.C00.mergeAt_single line 61
  15. def OAI.MarkovSuperreflexivity.prefixCut line 67
  16. theorem OAI.MarkovSuperreflexivity.prefixCut_zero line 69
  17. theorem OAI.MarkovSuperreflexivity.prefixCut_succ line 72