OAI/Analysis/MarkovType/FourLetters.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.Letter line 9
  2. def OAI.MarkovSuperreflexivity.Letter.inv line 13
  3. def OAI.MarkovSuperreflexivity.Letter.isPositive line 15
  4. def OAI.MarkovSuperreflexivity.Letter.isNegative line 17
  5. theorem OAI.MarkovSuperreflexivity.Letter.inv_inv line 19
  6. theorem OAI.MarkovSuperreflexivity.Letter.inv_ne_self line 23
  7. theorem OAI.MarkovSuperreflexivity.Letter.inv_injective line 27
  8. theorem OAI.MarkovSuperreflexivity.Letter.eq_inv_iff line 31
  9. theorem OAI.MarkovSuperreflexivity.card_letter line 36
  10. def OAI.MarkovSuperreflexivity.positiveCount line 39
  11. def OAI.MarkovSuperreflexivity.negativeCount line 41
  12. theorem OAI.MarkovSuperreflexivity.positiveCount_nil line 43
  13. theorem OAI.MarkovSuperreflexivity.negativeCount_nil line 45
  14. theorem OAI.MarkovSuperreflexivity.counts_nil line 47
  15. theorem OAI.MarkovSuperreflexivity.positiveCount_cons line 49
  16. theorem OAI.MarkovSuperreflexivity.negativeCount_cons line 53
  17. theorem OAI.MarkovSuperreflexivity.positiveCount_append line 57
  18. theorem OAI.MarkovSuperreflexivity.negativeCount_append line 61
  19. theorem OAI.MarkovSuperreflexivity.positiveCount_add_negativeCount line 65
  20. theorem OAI.MarkovSuperreflexivity.positiveCount_le_length line 73
  21. theorem OAI.MarkovSuperreflexivity.negativeCount_le_length line 76