OAI/Combinatorics/BalancedRyser/Candidates/CandidateSecondary.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateIncidence.generators line 14
  2. theorem OAI.Balanced.CandidateIncidence.generators_card line 17
  3. def OAI.Balanced.CandidateIncidence.generatorPairCandidates line 23
  4. def OAI.Balanced.CandidateIncidence.generatorConflicts line 27
  5. theorem OAI.Balanced.CandidateIncidence.generator_conflicts_card_le line 31
  6. def OAI.Balanced.CandidateIncidence.directionsAt line 52
  7. theorem OAI.Balanced.CandidateIncidence.directionsAt_card_le_multiplicity line 56
  8. theorem OAI.Balanced.CandidateIncidence.mem_directionsAt_iff line 59
  9. def OAI.Balanced.CandidateIncidence.touchedDirections line 72
  10. theorem OAI.Balanced.CandidateIncidence.mem_touchedDirections_iff line 75
  11. theorem OAI.Balanced.CandidateIncidence.touchedDirections_card_le line 85
  12. def OAI.Balanced.CandidateIncidence.mergedConflicts line 96
  13. theorem OAI.Balanced.CandidateIncidence.secondary_subset_generator_merged line 102
  14. def OAI.Balanced.CandidateIncidence.lineHitSlot line 140
  15. def OAI.Balanced.CandidateIncidence.mergedHitCandidates line 143
  16. theorem OAI.Balanced.CandidateIncidence.mergedHit_candidates_card_le line 147
  17. theorem OAI.Balanced.CandidateIncidence.merged_conflicts_card_le line 172
  18. theorem OAI.Balanced.CandidateIncidence.secondary_card_le line 194
  19. theorem OAI.Balanced.CandidateIncidence.E_inter_slot_eq_lineHitSlot line 204