OAI/Combinatorics/BalancedRyser/Selection/SelectionFinalLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Selection.Process.TailCheck line 14
  2. theorem OAI.Balanced.Selection.Process.tailCheck_iff line 21
  3. def OAI.Balanced.Selection.Process.failureLaw line 44
  4. theorem OAI.Balanced.Selection.Process.successMass_failureLaw line 50
  5. def OAI.Balanced.Selection.Process.recordedAssignment line 56
  6. theorem OAI.Balanced.Selection.Process.recordedAssignment_recorded line 60
  7. def OAI.Balanced.Selection.Process.terminalLaw line 70
  8. theorem OAI.Balanced.Selection.Process.successMass_terminalLaw line 96
  9. def OAI.Balanced.Selection.Process.terminalOutcomeLaw line 105
  10. def OAI.Balanced.Selection.Process.SourceTailCheck line 111
  11. def OAI.Balanced.Selection.Process.sourceTerminalLaw line 116
  12. theorem OAI.Balanced.Selection.Process.successMass_sourceTerminalLaw line 121
  13. def OAI.Balanced.Selection.Process.sourceTerminalOutcomeLaw line 130
  14. def OAI.Balanced.Selection.Process.finalLaw line 136
  15. theorem OAI.Balanced.Selection.Process.successMass_finalLaw line 155
  16. theorem OAI.Balanced.Selection.Process.cylinderMass_finalLaw line 177
  17. theorem OAI.Balanced.Selection.Process.occupancyFailureMass_finalLaw line 187
  18. theorem OAI.Balanced.Selection.Process.graphBounds_vertex_nonempty line 200
  19. def OAI.Balanced.Selection.Process.outputLaw line 210
  20. theorem OAI.Balanced.Selection.Process.outputLaw_eq_finalLaw line 214