OAI/Combinatorics/Progressions/Geometry/MixedRealCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.mixedRealCoordinates line 16
2. theorem OAI.Erdos3.mixedRealCoordinates_point line 21
3. theorem OAI.Erdos3.mixedRealPoint_coordinates line 30
4. theorem OAI.Erdos3.mixedRealCoordinates_integer line 38
5. theorem OAI.Erdos3.mixedRealCoordinates_norm_le line 44
6. theorem OAI.Erdos3.mixedRealCoordinates_lipschitz line 51