OAI/Computability/MinUncut/Analysis/Hermite.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.hermiteSupport line 21
  2. def OAI.MinUncut.Inner.matchingAxes line 23
  3. def OAI.MinUncut.Inner.forbiddenAxes line 26
  4. def OAI.MinUncut.Inner.goodAxes line 29
  5. lemma OAI.MinUncut.Inner.eq_of_two_faces line 32
  6. lemma OAI.MinUncut.Inner.matchingAxes_card line 39
  7. lemma OAI.MinUncut.Inner.hermiteSupport_card line 45
  8. lemma OAI.MinUncut.Inner.forbiddenAxes_card line 51
  9. lemma OAI.MinUncut.Inner.goodAxes_card line 61
  10. lemma OAI.MinUncut.Inner.goodAxis_no_support line 67
  11. lemma OAI.MinUncut.Inner.face_rowFill line 73
  12. lemma OAI.MinUncut.Inner.rowFill_axis line 77
  13. def OAI.MinUncut.Inner.rowObstructions line 80
  14. lemma OAI.MinUncut.Inner.obstruction_matching line 83
  15. lemma OAI.MinUncut.Inner.rowObstructions_card line 93
  16. def OAI.MinUncut.Inner.forbiddenPairs line 102
  17. lemma OAI.MinUncut.Inner.forbiddenPairs_card line 105
  18. lemma OAI.MinUncut.Inner.pair_not_forbidden_local line 112
  19. theorem OAI.MinUncut.Inner.admissible_pair line 122