OAI/Combinatorics/MatchingPSD/MatchingConversion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectMatchingPSD.pairingEdge line 9
  2. lemma OAI.PerfectMatchingPSD.pairingEdge_partner line 13
  3. lemma OAI.PerfectMatchingPSD.pairingEdge_incident line 20
  4. lemma OAI.PerfectMatchingPSD.pairingEdge_mem line 25
  5. lemma OAI.PerfectMatchingPSD.eq_pairingEdge line 30
  6. def OAI.PerfectMatchingPSD.fromPairing line 39
  7. lemma OAI.PerfectMatchingPSD.mem_fromPairing line 52
  8. lemma OAI.PerfectMatchingPSD.pairingEdge_cross line 56
  9. lemma OAI.PerfectMatchingPSD.cross_edge_inside line 61
  10. lemma OAI.PerfectMatchingPSD.pairingEdge_inside_injective line 71
  11. lemma OAI.PerfectMatchingPSD.crossingCount_fromPairing line 89
  12. lemma OAI.PerfectMatchingPSD.crossingCount_tableCoordinate line 104