OAI/Combinatorics/MatchingCount/Machines/TreeListMore.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.takeStep line 9
  2. def OAI.MatchingFPRAS.TreeTyped.takeStepRealizer line 14
  3. lemma OAI.MatchingFPRAS.TreeTyped.countDown_take line 22
  4. def OAI.MatchingFPRAS.TreeTyped.take line 33
  5. def OAI.MatchingFPRAS.TreeTyped.flatMap line 41
  6. def OAI.MatchingFPRAS.TreeTyped.minimum line 54
  7. def OAI.MatchingFPRAS.TreeTyped.maximum line 56
  8. def OAI.MatchingFPRAS.TreeTyped.listMin line 59
  9. def OAI.MatchingFPRAS.TreeTyped.listMinRealizer line 60
  10. lemma OAI.MatchingFPRAS.TreeTyped.listMin_le_default line 63
  11. lemma OAI.MatchingFPRAS.TreeTyped.listMin_le line 68
  12. lemma OAI.MatchingFPRAS.TreeTyped.le_listMin line 77