OAI/Combinatorics/BalancedRyser/Incidence/CandidateIncidence.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateIncidence.points line 16
  2. theorem OAI.Balanced.CandidateIncidence.valid line 19
  3. theorem OAI.Balanced.CandidateIncidence.points_card line 23
  4. theorem OAI.Balanced.CandidateIncidence.points_nonempty line 29
  5. theorem OAI.Balanced.CandidateIncidence.points_on_line line 35
  6. theorem OAI.Balanced.CandidateIncidence.eq_of_same_line_same_bit line 42
  7. theorem OAI.Balanced.CandidateIncidence.card_same_line_le_two line 50
  8. def OAI.Balanced.CandidateIncidence.exceptionalSet line 62
  9. theorem OAI.Balanced.CandidateIncidence.exceptional_subset line 66
  10. theorem OAI.Balanced.CandidateIncidence.exceptional_adjacent_or_same_slot line 69
  11. theorem OAI.Balanced.CandidateIncidence.not_exceptional_distinct_disjoint line 88
  12. theorem OAI.Balanced.CandidateIncidence.exceptional_card_le line 100
  13. def OAI.Balanced.CandidateIncidence.B line 124
  14. def OAI.Balanced.CandidateIncidence.E line 127
  15. theorem OAI.Balanced.CandidateIncidence.card_through_point_in_slot_le_one line 130
  16. theorem OAI.Balanced.CandidateIncidence.card_through_point_le line 141
  17. theorem OAI.Balanced.CandidateIncidence.B_slot_card_le_four line 158
  18. theorem OAI.Balanced.CandidateIncidence.B_card_le line 177
  19. theorem OAI.Balanced.CandidateIncidence.B_inter_B_card_le line 193
  20. def OAI.Balanced.CandidateIncidence.pointCandidates line 230
  21. def OAI.Balanced.CandidateIncidence.pointLineCandidates line 233
  22. def OAI.Balanced.CandidateIncidence.twoLineCandidates line 238
  23. theorem OAI.Balanced.CandidateIncidence.common_line_points_card_le_one line 242
  24. theorem OAI.Balanced.CandidateIncidence.pointLine_subset_of_onLine line 252
  25. theorem OAI.Balanced.CandidateIncidence.pointLine_card_le_of_onLine line 264
  26. theorem OAI.Balanced.CandidateIncidence.B_inter_E_card_le line 270
  27. theorem OAI.Balanced.CandidateIncidence.E_inter_E_card_le line 295
  28. theorem OAI.Balanced.CandidateIncidence.primary_common_card_le line 332
  29. def OAI.Balanced.CandidateIncidence.secondary line 357
  30. theorem OAI.Balanced.CandidateIncidence.neighbors_subset_primary_secondary line 360
  31. theorem OAI.Balanced.CandidateIncidence.common_neighbors_subset line 367
  32. theorem OAI.Balanced.CandidateIncidence.codegree_le_of_incidence_bounds line 378
  33. theorem OAI.Balanced.CandidateIncidence.degree_le_of_incidence_bounds line 399
  34. theorem OAI.Balanced.CandidateIncidence.slot_degree_le_of_incidence_bounds line 409