OAI/Combinatorics/MatchingCount/Machines/TreeRefreshNumbered.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableRefresh.sourceKey line 17
  2. def OAI.MatchingFPRAS.ExecutableRefresh.sourceCatalog line 19
  3. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceKey_injective line 21
  4. lemma OAI.MatchingFPRAS.ExecutableRefresh.index_lt line 32
  5. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceKey_le line 34
  6. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceCatalog_index line 56
  7. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceCatalog_pairwise line 69
  8. lemma OAI.MatchingFPRAS.ExecutableRefresh.source_inf_mem line 75
  9. lemma OAI.MatchingFPRAS.ExecutableRefresh.source_sup_mem line 80
  10. lemma OAI.MatchingFPRAS.ExecutableRefresh.edge_inf_lt_sup line 85
  11. def OAI.MatchingFPRAS.ExecutableRefresh.downEdge line 94
  12. lemma OAI.MatchingFPRAS.ExecutableRefresh.key_downEdge line 105
  13. def OAI.MatchingFPRAS.ExecutableRefresh.upEdge line 111
  14. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceKey_upEdge line 120
  15. lemma OAI.MatchingFPRAS.ExecutableRefresh.sourceCatalog_eq line 125