OAI/Combinatorics/Progressions/Geometry/SpatialTwoBlockEquiv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.twoKernelCopies line 11
2. def OAI.Erdos3.twoKernelEmbedding line 17
3. abbrev OAI.Erdos3.SpatialKernelRemainder line 20
4. def OAI.Erdos3.spatialTwoBlockEquiv line 23
5. theorem OAI.Erdos3.spatialTwoBlockEquiv_symm_first line 30
6. theorem OAI.Erdos3.spatialTwoBlockEquiv_symm_second line 34
7. theorem OAI.Erdos3.fixedSpatialKernelBlock_first line 38
8. theorem OAI.Erdos3.fixedSpatialKernelBlock_second line 43