OAI/Combinatorics/TriangleRemoval/Process/CompleteEdge.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpTerminalLeave.CompleteEdge line 15
  2. def OAI.SharpTerminalLeave.graphActive line 17
  3. lemma OAI.SharpTerminalLeave.mem_graphActive line 20
  4. def OAI.SharpTerminalLeave.graphEdgeEmbed line 23
  5. lemma OAI.SharpTerminalLeave.graphActive_sum line 26
  6. lemma OAI.SharpTerminalLeave.graphActive_card_le line 36
  7. lemma OAI.SharpTerminalLeave.graphActive_nested line 40
  8. def OAI.SharpTerminalLeave.graphRestrict line 44
  9. def OAI.SharpTerminalLeave.graphExtend line 50
  10. lemma OAI.SharpTerminalLeave.graphRestrict_extend line 55
  11. lemma OAI.SharpTerminalLeave.activeLinf_restrict line 61
  12. lemma OAI.SharpTerminalLeave.activeL2_restrict line 72
  13. def OAI.SharpTerminalLeave.graphMatrixLift line 79
  14. lemma OAI.SharpTerminalLeave.graphMatrixLift_restrict line 83
  15. lemma OAI.SharpTerminalLeave.graphMatrixLift_linf line 90
  16. lemma OAI.SharpTerminalLeave.graphMatrixLift_l2 line 98