OAI/Combinatorics/BalancedRyser/Selection/SelectionTailCompletion.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Selection.Process.Tail.Slot line 16
  2. abbrev OAI.Balanced.Selection.Process.Tail.Domain line 18
  3. def OAI.Balanced.Selection.Process.Tail.value line 21
  4. def OAI.Balanced.Selection.Process.Tail.graph line 23
  5. theorem OAI.Balanced.Selection.Process.Tail.value_slot line 27
  6. theorem OAI.Balanced.Selection.Process.Tail.value_injective line 32
  7. theorem OAI.Balanced.Selection.Process.Tail.value_mem_current line 43
  8. theorem OAI.Balanced.Selection.Process.Tail.card_domain line 49
  9. theorem OAI.Balanced.Selection.Process.Tail.noWithinSlotEdges line 55
  10. theorem OAI.Balanced.Selection.Process.Tail.degree_le line 65
  11. theorem OAI.Balanced.Selection.Process.Tail.tail_conditioning line 81
  12. def OAI.Balanced.Selection.Process.Tail.complete line 102
  13. theorem OAI.Balanced.Selection.Process.Tail.complete_remaining line 107
  14. theorem OAI.Balanced.Selection.Process.Tail.complete_recorded line 112
  15. theorem OAI.Balanced.Selection.Process.Tail.complete_agrees_recorded line 118
  16. theorem OAI.Balanced.Selection.Process.Tail.complete_isIndependentTransversal line 127
  17. def OAI.Balanced.Selection.Process.Tail.successfulAssignments line 155
  18. theorem OAI.Balanced.Selection.Process.Tail.mem_successfulAssignments line 161
  19. theorem OAI.Balanced.Selection.Process.Tail.successfulAssignments_nonempty line 169
  20. def OAI.Balanced.Selection.Process.Tail.completionPMF line 187
  21. theorem OAI.Balanced.Selection.Process.Tail.completionPMF_supported line 192
  22. theorem OAI.Balanced.Selection.Process.Tail.sum_pmf_real line 205
  23. def OAI.Balanced.Selection.Process.Tail.completionOutputLaw line 211
  24. theorem OAI.Balanced.Selection.Process.Tail.successMass_completionOutputLaw line 224