OAI/Combinatorics/BalancedRyser/Candidates/CandidateValidityAssembly.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateValidityAssembly.constituentFailures line 15
  2. def OAI.Balanced.CandidateValidityAssembly.oppositeFailures line 20
  3. def OAI.Balanced.CandidateValidityAssembly.externalFailures line 25
  4. theorem OAI.Balanced.CandidateValidityAssembly.successfulOn_of_mem line 30
  5. theorem OAI.Balanced.CandidateValidityAssembly.invalidPrescriptions_eq_union line 36
  6. theorem OAI.Balanced.CandidateValidityAssembly.invalidSuccessCount_le_failure_sum line 50
  7. def OAI.Balanced.CandidateValidityAssembly.prescriptionCode line 59
  8. theorem OAI.Balanced.CandidateValidityAssembly.prescriptionCode_injective line 63
  9. theorem OAI.Balanced.CandidateValidityAssembly.prescriptionCode_mem_constituentTargetCodes line 70
  10. theorem OAI.Balanced.CandidateValidityAssembly.constituentFailures_card_le line 91
  11. theorem OAI.Balanced.CandidateValidityAssembly.invalidSuccessCount_le line 99
  12. theorem OAI.Balanced.CandidateValidityAssembly.card_le_witnesses line 109
  13. theorem OAI.Balanced.CandidateValidityAssembly.invalidSuccessCount_le_witness_counts line 125
  14. theorem OAI.Balanced.CandidateValidityAssembly.candidateSlot_lower_bound_of_failures line 138