OAI/Combinatorics/TriangleRemoval/Queries/MarkedChild.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpTerminalLeave.MarkedChild line 17
  2. def OAI.SharpTerminalLeave.markedDemand line 22
  3. def OAI.SharpTerminalLeave.markedCheck line 26
  4. def OAI.SharpTerminalLeave.markedGood line 32
  5. def OAI.SharpTerminalLeave.markedFailure line 35
  6. theorem OAI.SharpTerminalLeave.markedGood_nonneg line 38
  7. theorem OAI.SharpTerminalLeave.markedGood_le_one line 43
  8. theorem OAI.SharpTerminalLeave.markedFailure_nonneg line 49
  9. def OAI.SharpTerminalLeave.markedBound line 54
  10. theorem OAI.SharpTerminalLeave.markedBound_nonneg line 59
  11. theorem OAI.SharpTerminalLeave.markedBound_of_no_demand line 70
  12. theorem OAI.SharpTerminalLeave.marked_visitation_bound line 79
  13. def OAI.SharpTerminalLeave.ordinaryCheck line 118
  14. theorem OAI.SharpTerminalLeave.markedCheck_original line 122