OAI/Combinatorics/BalancedRyser/Incidence/CandidateIncidenceInitialSums.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateIncidenceSums.admissibleCodes line 17
  2. def OAI.Balanced.CandidateIncidenceSums.probability line 21
  3. def OAI.Balanced.CandidateIncidenceSums.codeEvent line 26
  4. def OAI.Balanced.CandidateIncidenceSums.incidenceSum line 31
  5. theorem OAI.Balanced.CandidateIncidenceSums.probability_mono line 35
  6. theorem OAI.Balanced.CandidateIncidenceSums.mem_admissibleCodes line 47
  7. theorem OAI.Balanced.CandidateIncidenceSums.generators_fresh_of_mem_zero line 58
  8. theorem OAI.Balanced.CandidateIncidenceSums.card_admissibleCodes_le line 69
  9. theorem OAI.Balanced.CandidateIncidenceSums.card_direction_le_twice line 80
  10. theorem OAI.Balanced.CandidateIncidenceSums.sum_zero_le line 88
  11. theorem OAI.Balanced.CandidateIncidenceSums.sum_one_le line 112
  12. theorem OAI.Balanced.CandidateIncidenceSums.code_probability_le_alignment line 137
  13. def OAI.Balanced.CandidateIncidenceSums.designatesPoint line 144
  14. def OAI.Balanced.CandidateIncidenceSums.throughPointHitsLine line 147
  15. def OAI.Balanced.CandidateIncidenceSums.hitsTwoLines line 151
  16. theorem OAI.Balanced.CandidateIncidenceSums.point_sum_zero_le line 154
  17. theorem OAI.Balanced.CandidateIncidenceSums.point_sum_one_le line 165
  18. theorem OAI.Balanced.CandidateIncidenceSums.point_line_sum_zero_le line 177
  19. theorem OAI.Balanced.CandidateIncidenceSums.point_line_sum_one_le line 190
  20. theorem OAI.Balanced.CandidateIncidenceSums.two_lines_sum_zero_le line 203
  21. theorem OAI.Balanced.CandidateIncidenceSums.two_lines_sum_one_le line 215