OAI/Combinatorics/Progressions/Lattices/IntegerBoxCoordinateEquiv.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateReindexedSides line 13
  2. def OAI.Erdos3.coordinateReindexedFunction line 16
  3. theorem OAI.Erdos3.coordinateReindexedSides_mem_integerBox line 21
  4. theorem OAI.Erdos3.coordinateReindexedFunction_expect line 31
  5. theorem OAI.Erdos3.coordinateReindexedFunction_bounds line 50
  6. theorem OAI.Erdos3.coordinateReindexedFunction_apFree line 57
  7. def OAI.Erdos3.integerPointCoordinateEquiv line 87
  8. theorem OAI.Erdos3.integerPointCoordinateEquiv_apply line 93
  9. theorem OAI.Erdos3.integerPointCoordinateEquiv_symm_apply line 96
  10. theorem OAI.Erdos3.integerPointCoordinateEquiv_symm line 99
  11. theorem OAI.Erdos3.integerPointCoordinateEquiv_mem_integerBox line 104
  12. def OAI.Erdos3.integerBoxCoordinateEquiv line 111
  13. theorem OAI.Erdos3.integerBoxCoordinateEquiv_val line 120
  14. theorem OAI.Erdos3.integerBoxCoordinateEquiv_symm_val line 124
  15. theorem OAI.Erdos3.integerBox_map_coordinateEquiv line 129
  16. theorem OAI.Erdos3.integerBox_image_coordinateEquiv line 142