OAI/Combinatorics/MatchingCount/Sampling/TreeIndexedPairCorrect.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutablePair.endpointRep line 11
  2. def OAI.MatchingFPRAS.ExecutablePair.contextRep line 12
  3. lemma OAI.MatchingFPRAS.ExecutablePair.endpoints_rep line 16
  4. lemma OAI.MatchingFPRAS.ExecutablePair.u_rep line 19
  5. lemma OAI.MatchingFPRAS.ExecutablePair.v_rep line 22
  6. lemma OAI.MatchingFPRAS.ExecutablePair.pair_inf_sup line 26
  7. lemma OAI.MatchingFPRAS.ExecutablePair.incident_rep line 27
  8. lemma OAI.MatchingFPRAS.ExecutablePair.same_rep line 35
  9. lemma OAI.MatchingFPRAS.ExecutablePair.same_pair_rep line 40
  10. lemma OAI.MatchingFPRAS.ExecutablePair.adjacent_rep line 45
  11. lemma OAI.MatchingFPRAS.ExecutablePair.p_rep line 62
  12. lemma OAI.MatchingFPRAS.ExecutablePair.q_rep line 66
  13. lemma OAI.MatchingFPRAS.ExecutablePair.r_rep line 70
  14. lemma OAI.MatchingFPRAS.ExecutablePair.t_rep line 74