OAI/Combinatorics/MatchingCount/Algorithm/TreeGeneratedPrepared.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableSource.rangeFromList line 14
  2. def OAI.MatchingFPRAS.ExecutableSource.rangeFromListRealizer line 15
  3. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_rangeFromList line 17
  4. lemma OAI.MatchingFPRAS.ExecutableSource.range_card_set line 21
  5. def OAI.MatchingFPRAS.ExecutableSource.sourceVertices line 31
  6. def OAI.MatchingFPRAS.ExecutableSource.sourceVerticesRealizer line 32
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sourceVertices line 34
  8. lemma OAI.MatchingFPRAS.ExecutableSource.sourceVertices_length line 37
  9. def OAI.MatchingFPRAS.ExecutableSource.sourceEdgeData line 44
  10. def OAI.MatchingFPRAS.ExecutableSource.sourceEdgeDataRealizer line 46
  11. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sourceEdgeData line 50
  12. lemma OAI.MatchingFPRAS.ExecutableSource.sourceCatalog_endpoints line 59
  13. lemma OAI.MatchingFPRAS.ExecutableSource.sourceEdgeData_source line 65
  14. abbrev OAI.MatchingFPRAS.ExecutableSource.GeneratedInput line 81
  15. def OAI.MatchingFPRAS.ExecutableSource.generatedTier line 82
  16. def OAI.MatchingFPRAS.ExecutableSource.generatedTierRealizer line 84
  17. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedTier line 87
  18. def OAI.MatchingFPRAS.ExecutableSource.generatedPrepared line 95
  19. def OAI.MatchingFPRAS.ExecutableSource.generatedPreparedRealizer line 97
  20. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedPrepared line 100
  21. lemma OAI.MatchingFPRAS.ExecutableSource.generatedPrepared_source line 109
  22. theorem OAI.MatchingFPRAS.ExecutableSource.generatedPrepared_post line 125