OAI/Combinatorics/TriangleRemoval/Queries/MarkedSuccess.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.markedSuccess line 18
  2. theorem OAI.SharpTerminalLeave.markedFailure_eq_one_sub line 21
  3. def OAI.SharpTerminalLeave.selectedClockLaw line 29
  4. theorem OAI.SharpTerminalLeave.selectedClockLaw_support line 33
  5. def OAI.SharpTerminalLeave.rowChild line 41
  6. def OAI.SharpTerminalLeave.markedRow line 47
  7. theorem OAI.SharpTerminalLeave.markedRow_sorted line 53
  8. theorem OAI.SharpTerminalLeave.markedRow_factor_product line 63
  9. theorem OAI.SharpTerminalLeave.markedRow_pointwise line 73
  10. theorem OAI.SharpTerminalLeave.markedRow_integrated line 99