OAI/Combinatorics/Ryser/Selection/CertificateUnion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Selection.not_hasCompatibleChoice_mem_certificate_union line 15
  2. theorem OAI.RyserCoveringCounterexample.Selection.prob_not_hasCompatibleChoice_le_certificate_sum line 29
  3. theorem OAI.RyserCoveringCounterexample.Selection.sum_certificate_probs_le line 54
  4. theorem OAI.RyserCoveringCounterexample.Selection.sum_certificate_probs_card_eq_le line 76
  5. theorem OAI.RyserCoveringCounterexample.Selection.not_hasCompatibleChoice_mem_size_union line 108
  6. theorem OAI.RyserCoveringCounterexample.Selection.prob_not_hasCompatibleChoice_le_grouped_certificate_sum line 125
  7. theorem OAI.RyserCoveringCounterexample.Selection.prob_not_hasCompatibleChoice_le_size_sum line 164