OAI/Combinatorics/BalancedRyser/Construction/ConstructionBlockCardinality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.BlockCardinality.block_nonempty line 14
  2. theorem OAI.Balanced.BlockCardinality.lines_in_direction_card line 46
  3. theorem OAI.Balanced.BlockCardinality.constituents_in_direction line 58
  4. theorem OAI.Balanced.BlockCardinality.constituents_in_direction_card line 78
  5. theorem OAI.Balanced.BlockCardinality.split_constituents_disjoint line 86
  6. theorem OAI.Balanced.BlockCardinality.nonregular_in_direction_card line 93
  7. theorem OAI.Balanced.BlockCardinality.regular_lines_card line 100
  8. theorem OAI.Balanced.BlockCardinality.four_le_field_card line 110
  9. def OAI.Balanced.BlockCardinality.splitLabels line 121
  10. theorem OAI.Balanced.BlockCardinality.labels_in_direction_eq line 124
  11. theorem OAI.Balanced.BlockCardinality.split_labels_card line 143
  12. theorem OAI.Balanced.BlockCardinality.labels_in_direction_card line 151