OAI/Combinatorics/BalancedRyser/Incidence/ParallelPencilForcing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.parallel_mem_linePoints_iff line 13
  2. theorem OAI.Balanced.missing_parallel_line_cover line 16
  3. theorem OAI.Balanced.parallel_trace_card_le_one line 31
  4. theorem OAI.Balanced.missing_parallel_trace_bound line 42
  5. theorem OAI.Balanced.missing_parallel_line_occupancy_bound line 51
  6. theorem OAI.Balanced.Configuration.parallel_pencil_line_is_represented line 68
  7. theorem OAI.Balanced.Configuration.parallel_direction_card line 98
  8. theorem OAI.Balanced.Configuration.parallel_nondeleted_card line 105
  9. theorem OAI.Balanced.Configuration.parallel_pencil_forced_label_count line 116
  10. theorem OAI.Balanced.Configuration.parallel_pencil_remaining_labels_le_three line 141