OAI/Combinatorics/MatchingPSD/GlobalGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingSmoothing.abColor line 14
  2. def OAI.MatchingSmoothing.threeColor line 15
  3. def OAI.MatchingSmoothing.crossVector line 16
  4. lemma OAI.MatchingSmoothing.crossVector_sum line 19
  5. lemma OAI.MatchingSmoothing.threeColor_closed line 36
  6. def OAI.MatchingSmoothing.starFiberEquiv line 49
  7. def OAI.MatchingSmoothing.insertCellEquiv line 63
  8. def OAI.MatchingSmoothing.localSplitEquiv line 74
  9. def OAI.MatchingSmoothing.extendLocal line 77
  10. def OAI.MatchingSmoothing.liftLocal line 81
  11. lemma OAI.MatchingSmoothing.extendLocal_relabel line 85
  12. lemma OAI.MatchingSmoothing.localSplit_inl line 91
  13. lemma OAI.MatchingSmoothing.localSplit_cell line 93
  14. lemma OAI.MatchingSmoothing.localSplit_outside line 95
  15. lemma OAI.MatchingSmoothing.extendLocal_sum line 98