OAI/Combinatorics/Progressions/Estimates/AmbientImageExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.rightCosetMetricSpace_image_ball line 17
2. theorem OAI.Erdos3.rightCosetMetricSpace_exists_lift line 32
3. theorem OAI.Erdos3.cosetImage_local_lifts line 57
4. theorem OAI.Erdos3.exists_lipschitz_cosetImage_reconstruction line 115
5. theorem OAI.Erdos3.quotient_local_lifts_of_identity_lifts line 153
6. theorem OAI.Erdos3.exists_lipschitz_observable_reconstruction line 191
7. theorem OAI.Erdos3.exists_ambient_image_reconstruction line 229