OAI/Combinatorics/MatchingCount/Sampling/TreeUnitDraw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableUnit.decodeIndex line 10
  2. def OAI.MatchingFPRAS.ExecutableUnit.decodeIndexRealizer line 11
  3. def OAI.MatchingFPRAS.ExecutableUnit.probability line 13
  4. def OAI.MatchingFPRAS.ExecutableUnit.probabilityRealizer line 15
  5. def OAI.MatchingFPRAS.ExecutableUnit.probabilities line 21
  6. def OAI.MatchingFPRAS.ExecutableUnit.probabilitiesRealizer line 23
  7. def OAI.MatchingFPRAS.ExecutableUnit.draw line 29
  8. def OAI.MatchingFPRAS.ExecutableUnit.drawRealizer line 31
  9. lemma OAI.MatchingFPRAS.ExecutableUnit.decodeIndex_fin line 36
  10. lemma OAI.MatchingFPRAS.ExecutableUnit.probabilities_eq line 39
  11. lemma OAI.MatchingFPRAS.ExecutableUnit.draw_eq line 55