OAI/Combinatorics/Progressions/Geometry/RightCosetMetricMap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.quotientRightEDist_image_eball line 14
  2. theorem OAI.Erdos3.quotientRightEDist_nhds_basis line 35
  3. def OAI.Erdos3.rightCosetPseudoEMetricSpace line 44
  4. theorem OAI.Erdos3.rightCosetPseudoEMetricSpace_topology line 49
  5. def OAI.Erdos3.rightCosetEMetricSpace line 54
  6. theorem OAI.Erdos3.rightCosetEMetricSpace_topology line 60
  7. def OAI.Erdos3.rightCosetMetricSpace line 73
  8. theorem OAI.Erdos3.rightCosetMetricSpace_topology line 84
  9. theorem OAI.Erdos3.rightCosetMetricSpace_edist_mk line 88
  10. theorem OAI.Erdos3.rightCosetMetricSpace_lipschitz_mk line 92
  11. def OAI.Erdos3.cosetMap line 112
  12. theorem OAI.Erdos3.cosetMap_mk line 119
  13. theorem OAI.Erdos3.cosetMap_surjective line 123
  14. theorem OAI.Erdos3.rightCosetEDist_map_le line 134
  15. theorem OAI.Erdos3.quotientRightEDist_map_le line 149
  16. theorem OAI.Erdos3.lipschitz_cosetMap line 165