OAI/Combinatorics/BalancedRyser/Candidates/CandidateOldExternalOverlap.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateOldExternal.targetLine line 14
  2. theorem OAI.Balanced.CandidateOldExternal.successfulOn_target line 17
  3. def OAI.Balanced.CandidateOldExternal.IsExternalWitness line 27
  4. abbrev OAI.Balanced.CandidateOldExternal.WitnessKey line 33
  5. abbrev OAI.Balanced.CandidateOldExternal.WitnessLabel line 36
  6. def OAI.Balanced.CandidateOldExternal.oldOverlapKeys line 38
  7. def OAI.Balanced.CandidateOldExternal.oldOverlapWitnesses line 43
  8. theorem OAI.Balanced.CandidateOldExternal.mem_oldOverlapWitnesses_iff line 48
  9. theorem OAI.Balanced.CandidateOldExternal.key_injective_on_oldOverlapWitnesses line 58
  10. theorem OAI.Balanced.CandidateOldExternal.card_oldOverlapWitnesses_le line 72
  11. theorem OAI.Balanced.CandidateOldExternal.exists_mem_of_old_external line 86
  12. theorem OAI.Balanced.CandidateOldExternal.expected_oldOverlapWitnesses_le line 96
  13. def OAI.Balanced.CandidateOldExternal.oldOverlapPrescriptions line 124
  14. def OAI.Balanced.CandidateOldExternal.keyEvent line 129
  15. theorem OAI.Balanced.CandidateOldExternal.keyWitnesses_eq_image line 133
  16. theorem OAI.Balanced.CandidateOldExternal.keyWitnesses_card line 161
  17. theorem OAI.Balanced.CandidateOldExternal.sum_oldOverlapWitness_probability_le line 168