OAI/Combinatorics/Progressions/Geometry/SpatialStarCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.spatialStar line 11
2. def OAI.Erdos3.spatialUnstar line 14
3. theorem OAI.Erdos3.spatialUnstar_star line 17
4. theorem OAI.Erdos3.spatialStar_unstar line 24
5. theorem OAI.Erdos3.spatialUnstar_lipschitz line 31
6. theorem OAI.Erdos3.spatialUnstar_scaled_star line 51
7. theorem OAI.Erdos3.spatialUnstar_residue_star line 58
8. def OAI.Erdos3.spatialStarVertex line 65
9. theorem OAI.Erdos3.spatialStar_vertex line 68