OAI/Combinatorics/Progressions/Geometry/CommonNativeCoordinateCorrections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.spaces_le_fourHorizontalLayer line 24
2. def OAI.Erdos3.NativeRankRelation.CommonData.coordinateSpace line 36
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.coordinateSpace_eq_map line 41
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coordinate_generators line 46
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_bounded_coordinate_generators line 89
6. def OAI.Erdos3.NativeRankRelation.CommonData.realCoordinateSpace line 130
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.realCoordinateSpace_eq_image line 134
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.realCoordinateSpace_mem line 139
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coordinate_corrections line 167
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_uniform_native_coordinate_corrections line 222