OAI/Combinatorics/Progressions/Estimates/RectangularCellGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.rectangularLatticeCell_disjoint line 9
2. theorem OAI.Erdos3.rectangularLatticePoint_mem_cell line 18
3. theorem OAI.Erdos3.rectangularLatticeCell_point_distance line 26
4. theorem OAI.Erdos3.integerBoxCell_unit_bound line 36