OAI/Combinatorics/MatchingCount/Tapes/TreeSparseComponents.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.adjacent line 13
  2. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.adjacentRealizer line 16
  3. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_adjacent line 27
  4. abbrev OAI.MatchingFPRAS.TreeTyped.SparseProgram.ComponentInput line 32
  5. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.component line 34
  6. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.componentRealizer line 36
  7. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_component line 42
  8. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.orderedSetEqual line 55
  9. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_orderedSetEqual line 58
  10. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.allComponents line 62
  11. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.allComponentsRealizer line 64
  12. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_allComponents line 69
  13. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.discrepancies line 79
  14. def OAI.MatchingFPRAS.TreeTyped.SparseProgram.discrepanciesRealizer line 81
  15. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_discrepancies line 89
  16. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.adjacent_eq line 110
  17. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.component_eq line 115
  18. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.allComponents_eq line 119
  19. lemma OAI.MatchingFPRAS.TreeTyped.SparseProgram.discrepancies_eq line 123