OAI/Combinatorics/Progressions/Geometry/CubeSignalCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fullCubeSignal line 11
  2. theorem OAI.Erdos3.booleanWeight_true line 15
  3. theorem OAI.Erdos3.cubeShift_true line 18
  4. theorem OAI.Erdos3.exists_false_of_ne_true line 21
  5. theorem OAI.Erdos3.cubeShift_congr_selected line 27
  6. theorem OAI.Erdos3.fullCube_input_independent line 37
  7. theorem OAI.Erdos3.mixedCubeInput_independent line 53
  8. theorem OAI.Erdos3.mixedCubeInput_true line 72
  9. theorem OAI.Erdos3.fullCubeSignal_profile line 78