OAI/Combinatorics/MatchingCount/Machines/TreeFinite.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.Realizer.recode line 12
  2. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_recode line 21
  3. instance OAI.MatchingFPRAS.TreeTyped.finsetCodec line 30
  4. lemma OAI.MatchingFPRAS.TreeTyped.encode_finset line 31
  5. lemma OAI.MatchingFPRAS.TreeTyped.weight_finset line 32
  6. def OAI.MatchingFPRAS.TreeTyped.finsetList line 35
  7. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetList line 37
  8. def OAI.MatchingFPRAS.TreeTyped.listFinset line 41
  9. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_listFinset line 46
  10. def OAI.MatchingFPRAS.TreeTyped.finsetMember line 52
  11. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetMember line 55
  12. def OAI.MatchingFPRAS.TreeTyped.finsetCard line 60
  13. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetCard line 62
  14. def OAI.MatchingFPRAS.TreeTyped.finsetUnion line 66
  15. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetUnion line 71
  16. def OAI.MatchingFPRAS.TreeTyped.finsetImage line 80
  17. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetImage line 85
  18. lemma OAI.MatchingFPRAS.TreeTyped.sort_filter line 94
  19. def OAI.MatchingFPRAS.TreeTyped.finsetFilter line 100
  20. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetFilter line 104
  21. def OAI.MatchingFPRAS.TreeTyped.finsetFilterWith line 109
  22. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_filterWith line 116
  23. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_finsetFilterWith line 122