OAI/Combinatorics/Progressions/Geometry/PrincipalCubeSupportedCell.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.principalSupportedResidue_restrict line 31
  2. theorem OAI.Erdos3.containedSupportedProgressionLaw_restrict line 54
  3. def OAI.Erdos3.containedSupportedProgressionAxisLaw line 102
  4. theorem OAI.Erdos3.containedSupportedProgressionLaw_partition line 109
  5. theorem OAI.Erdos3.containedSupportedProgressionAxisLaw_eq_of_size line 145
  6. theorem OAI.Erdos3.containedSupportedProgressionAxisLaw_cube_support line 158
  7. theorem OAI.Erdos3.containedSupportedProgressionLaw_partition_comparison line 168
  8. theorem OAI.Erdos3.containedSupportedProgressionLaw_axis_marginal line 180
  9. theorem OAI.Erdos3.containedSupportedProgressionLaw_integral_comparison line 242
  10. theorem OAI.Erdos3.principalTupleWeights_weight_pos_of_cube line 272
  11. theorem OAI.Erdos3.principalResidueCell_pos_of_cube line 283
  12. theorem OAI.Erdos3.principalAxisJoin_cube line 293