OAI/Combinatorics/BalancedRyser/Selection/SelectionCensoring.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.card_le_filter_add_two line 13
  2. theorem OAI.Balanced.Selection.card_le_filter_add_three line 26
  3. theorem OAI.Balanced.Selection.Process.mem_currentVertices_update_iff line 55
  4. theorem OAI.Balanced.Selection.Process.currentVertices_update_subset line 66
  5. theorem OAI.Balanced.Selection.Process.exceptional_not_mem_currentVertices_update line 72
  6. theorem OAI.Balanced.Selection.Process.postcheck_of_performedResult_some line 86
  7. theorem OAI.Balanced.Selection.Process.update_eq_of_performedResult_some line 94
  8. theorem OAI.Balanced.Selection.Process.performedResult_none_of_domain_overflow line 102
  9. theorem OAI.Balanced.Selection.Process.performedResult_none_of_degree_overflow line 112
  10. theorem OAI.Balanced.Selection.Process.relevant_successor_uncensored line 121
  11. theorem OAI.Balanced.Selection.Process.domain_loss_le_conflicts_add_thinning line 138
  12. theorem OAI.Balanced.Selection.Process.domain_loss_le_two_mul_rpow line 165
  13. theorem OAI.Balanced.Selection.Process.degree_loss_le_three_counts line 187
  14. theorem OAI.Balanced.Selection.Process.degree_loss_le_three_mul_rpow line 226
  15. theorem OAI.Balanced.Selection.Process.degree_update_le line 241
  16. theorem OAI.Balanced.Selection.Process.abs_degree_update_sub_le_three_mul_rpow line 247
  17. theorem OAI.Balanced.Selection.Process.currentVertices_subset_of_performed_steps line 261
  18. theorem OAI.Balanced.Selection.Process.exceptional_not_relevant_later line 283
  19. theorem OAI.Balanced.Selection.Process.relevant_final_uncensored_at line 298
  20. theorem OAI.Balanced.Selection.Process.domain_update_eq_survivors_inter_domain line 314