OAI/Combinatorics/Progressions/Linear/BooleanCubeCoordinateFrame.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.affineSite line 14
  2. def OAI.Erdos3.BooleanCubeKernel.frameCoordinate line 19
  3. def OAI.Erdos3.BooleanCubeKernel.liftCoordinate line 25
  4. def OAI.Erdos3.BooleanCubeKernel.frameProjection line 30
  5. def OAI.Erdos3.BooleanCubeKernel.frameLift line 35
  6. theorem OAI.Erdos3.BooleanCubeKernel.frameProjection_lift line 40
  7. theorem OAI.Erdos3.BooleanCubeKernel.liftCoordinate_homogeneous line 55
  8. theorem OAI.Erdos3.BooleanCubeKernel.frameLift_homogeneous line 66
  9. theorem OAI.Erdos3.BooleanCubeKernel.frameCoordinate_homogeneous line 73
  10. theorem OAI.Erdos3.BooleanCubeKernel.frameCoordinate_eval line 85
  11. theorem OAI.Erdos3.BooleanCubeKernel.frameProjection_eval line 100