OAI/Computability/MatchingCount/RawData.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Raw.Matrix line 9
  2. abbrev OAI.BinaryMatching.Raw.Cut line 10
  3. abbrev OAI.BinaryMatching.Raw.Paths line 11
  4. def OAI.BinaryMatching.Raw.nth line 13
  5. def OAI.BinaryMatching.Raw.get line 14
  6. def OAI.BinaryMatching.Raw.tab line 15
  7. def OAI.BinaryMatching.Raw.matrix line 16
  8. def OAI.BinaryMatching.Raw.view line 17
  9. def OAI.BinaryMatching.Raw.mem line 19
  10. def OAI.BinaryMatching.Raw.empty line 20
  11. def OAI.BinaryMatching.Raw.full line 21
  12. def OAI.BinaryMatching.Raw.inter line 22
  13. def OAI.BinaryMatching.Raw.compl line 23
  14. def OAI.BinaryMatching.Raw.cardinal line 24
  15. def OAI.BinaryMatching.Raw.vectorRep line 26
  16. def OAI.BinaryMatching.Raw.matrixRep line 27
  17. def OAI.BinaryMatching.Raw.cutRep line 29
  18. def OAI.BinaryMatching.Raw.pathRep line 30
  19. lemma OAI.BinaryMatching.Raw.tab_eq_ofFn line 33
  20. lemma OAI.BinaryMatching.Raw.range_eq_fin line 40
  21. lemma OAI.BinaryMatching.Raw.at_rep line 44
  22. lemma OAI.BinaryMatching.Raw.get_rep line 47
  23. lemma OAI.BinaryMatching.Raw.mem_rep line 50
  24. lemma OAI.BinaryMatching.Raw.tab_eq_rep line 53
  25. lemma OAI.BinaryMatching.Raw.matrix_eq_rep line 56
  26. lemma OAI.BinaryMatching.Raw.empty_rep line 62
  27. lemma OAI.BinaryMatching.Raw.full_rep line 64
  28. lemma OAI.BinaryMatching.Raw.inter_rep line 66
  29. lemma OAI.BinaryMatching.Raw.compl_rep line 71
  30. lemma OAI.BinaryMatching.Raw.cardinal_rep line 75
  31. lemma OAI.BinaryMatching.Raw.sum_tab line 86