OAI/Combinatorics/BalancedRyser/Construction/BlockPartitions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Configuration.BlockPartitions.line_eq_of_direction_eq line 13
  2. theorem OAI.Balanced.Configuration.BlockPartitions.split_direction line 18
  3. theorem OAI.Balanced.Configuration.BlockPartitions.split_not_constituent line 21
  4. theorem OAI.Balanced.Configuration.BlockPartitions.tuple_injective line 24
  5. theorem OAI.Balanced.Configuration.BlockPartitions.tuple_on_split line 28
  6. theorem OAI.Balanced.Configuration.BlockPartitions.point_on_split_designated line 32
  7. theorem OAI.Balanced.Configuration.BlockPartitions.split_line_injective line 44
  8. theorem OAI.Balanced.Configuration.BlockPartitions.split_block_onLine line 54
  9. theorem OAI.Balanced.Configuration.BlockPartitions.split_block_side_unique line 61
  10. theorem OAI.Balanced.Configuration.BlockPartitions.constituent_mem line 80
  11. theorem OAI.Balanced.Configuration.BlockPartitions.regular_block_onLine line 84
  12. theorem OAI.Balanced.Configuration.BlockPartitions.merged_block_onLine line 88
  13. theorem OAI.Balanced.Configuration.BlockPartitions.regular_split_disjoint line 95
  14. theorem OAI.Balanced.Configuration.BlockPartitions.regular_merged_disjoint line 105
  15. theorem OAI.Balanced.Configuration.BlockPartitions.merged_split_disjoint line 117
  16. theorem OAI.Balanced.Configuration.BlockPartitions.block_unique line 128
  17. theorem OAI.Balanced.Configuration.BlockPartitions.block_exists line 154
  18. theorem OAI.Balanced.Configuration.BlockPartitions.existsUnique_block line 194
  19. def OAI.Balanced.Configuration.BlockPartitions.pointLabel line 202
  20. theorem OAI.Balanced.Configuration.BlockPartitions.pointLabel_mem line 208
  21. theorem OAI.Balanced.Configuration.BlockPartitions.pointLabel_eq_iff line 213