OAI/Combinatorics/Progressions/Geometry/ChartCutoff.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.chartCutoff line 14
2. theorem OAI.Erdos3.chartCutoff_apply line 19
3. theorem OAI.Erdos3.chartCutoff_range line 24
4. theorem OAI.Erdos3.tsupport_chartCutoff_subset line 32
5. theorem OAI.Erdos3.hasCompactSupport_chartCutoff line 45
6. theorem OAI.Erdos3.lipschitz_chartCutoff line 52