OAI/Combinatorics/BalancedRyser/Construction/ValidChoice.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.SplitGeometry.adjacent_symm line 14
  2. theorem OAI.Balanced.SplitGeometry.intersection_on_left line 20
  3. theorem OAI.Balanced.SplitGeometry.intersection_on_right line 25
  4. theorem OAI.Balanced.SplitGeometry.valid_card_designated line 47
  5. theorem OAI.Balanced.SplitGeometry.valid_no_opposite line 50
  6. theorem OAI.Balanced.SplitGeometry.valid_external_unique line 60
  7. theorem OAI.Balanced.SplitGeometry.valid_exists_uncovered line 70
  8. theorem OAI.Balanced.SplitGeometry.valid_not_covered line 81
  9. theorem OAI.Balanced.SplitGeometry.valid_consecutive_adjacent line 91
  10. theorem OAI.Balanced.SplitGeometry.adjacent_mem_merged line 118
  11. theorem OAI.Balanced.SplitGeometry.valid_common_block_or_merged line 127
  12. theorem OAI.Balanced.SplitGeometry.selected_designated_mem_points line 139
  13. theorem OAI.Balanced.SplitGeometry.selected_pair_common_block line 144