OAI/Combinatorics/Progressions/Estimates/ReindexedCubeDomain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.coordinateReindex_measurePreserving line 11
2. def OAI.Erdos3.reindexedBlockCubeDomain line 18
3. theorem OAI.Erdos3.reindexedBlockCubeDomain_measurable line 22
4. theorem OAI.Erdos3.reindexedBlockCubeDomain_box line 27
5. theorem OAI.Erdos3.blockCubeMeasure_real_reindex line 33