OAI/Combinatorics/MatchingCount/Machines/TreeFiniteOps.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.all line 11
  2. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_all line 18
  3. def OAI.MatchingFPRAS.TreeTyped.pairEqual line 23
  4. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_pairEqual line 32
  5. def OAI.MatchingFPRAS.TreeTyped.leNat line 41
  6. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_leNat line 46
  7. def OAI.MatchingFPRAS.TreeTyped.finsetAny line 52
  8. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetAny line 58
  9. def OAI.MatchingFPRAS.TreeTyped.finsetAll line 65
  10. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetAll line 71
  11. def OAI.MatchingFPRAS.TreeTyped.finsetSubset line 78
  12. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetSubset line 82
  13. def OAI.MatchingFPRAS.TreeTyped.finsetEqual line 88
  14. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetEqual line 94
  15. def OAI.MatchingFPRAS.TreeTyped.finsetSDiff line 100
  16. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetSDiff line 104
  17. def OAI.MatchingFPRAS.TreeTyped.finsetInter line 111
  18. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetInter line 117
  19. def OAI.MatchingFPRAS.TreeTyped.finsetErase line 124
  20. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetErase line 130