OAI/Combinatorics/BalancedRyser/Probability/ConfigurationStructure.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ConfigurationStructure.choice_line_mem_split line 15
  2. theorem OAI.Balanced.ConfigurationStructure.choice_designated_subset line 18
  3. theorem OAI.Balanced.ConfigurationStructure.choice_designated_card line 25
  4. theorem OAI.Balanced.ConfigurationStructure.choice_designated_disjoint line 30
  5. theorem OAI.Balanced.ConfigurationStructure.designated_slot_unique line 40
  6. theorem OAI.Balanced.ConfigurationStructure.choice_line_injective line 46
  7. theorem OAI.Balanced.ConfigurationStructure.retained_subset_points line 55
  8. theorem OAI.Balanced.ConfigurationStructure.core_subset_retained line 57
  9. theorem OAI.Balanced.ConfigurationStructure.core_subset_points line 64
  10. theorem OAI.Balanced.ConfigurationStructure.designated_subset_points line 67
  11. theorem OAI.Balanced.ConfigurationStructure.split_inter_points line 72
  12. theorem OAI.Balanced.ConfigurationStructure.split_lines_card line 90
  13. theorem OAI.Balanced.ConfigurationStructure.split_multiplicity_eq_slots line 96
  14. theorem OAI.Balanced.ConfigurationStructure.designated_at_card line 103
  15. theorem OAI.Balanced.ConfigurationStructure.split_multiplicity_le_one_of_designated line 114
  16. theorem OAI.Balanced.ConfigurationStructure.center_not_designated line 127
  17. theorem OAI.Balanced.ConfigurationStructure.split_lines_in_direction line 134
  18. theorem OAI.Balanced.ConfigurationStructure.split_pair_ne line 156
  19. theorem OAI.Balanced.ConfigurationStructure.split_lines_in_direction_card line 163
  20. theorem OAI.Balanced.ConfigurationStructure.choice_line_ne_constituent line 168
  21. theorem OAI.Balanced.ConfigurationStructure.deleted_lines_in_direction line 175
  22. theorem OAI.Balanced.ConfigurationStructure.deleted_lines_in_direction_card line 209