OAI/Geometry/Cannon/Topology/CenteredHomeomorph.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonPlane.segment_isCompact line 43
  2. lemma OAI.CannonPlane.segment_isConnected line 47
  3. lemma OAI.CannonPlane.ray_image_escapes line 51
  4. lemma OAI.CannonPlane.norm_ge_of_mem_radial_segment line 69
  5. theorem OAI.CannonPlane.annular_ratio line 77
  6. def OAI.CannonPlane.centeredHomeomorph line 138
  7. lemma OAI.CannonPlane.centeredHomeomorph_apply line 146
  8. lemma OAI.CannonPlane.centeredHomeomorph_symm_apply line 149
  9. lemma OAI.CannonPlane.centered_symm_contDiff line 152
  10. lemma OAI.CannonPlane.centered_symm_fderiv line 156
  11. theorem OAI.CannonPlane.annular_ratio_at line 163
  12. theorem OAI.CannonPlane.smooth_qc_uniform_shrink line 177
  13. def OAI.CannonPlane.UniformRelativeControl line 238
  14. theorem OAI.CannonPlane.normalized_family_pointwise_bound line 242
  15. theorem OAI.CannonPlane.relative_control_equicontinuous line 286
  16. def OAI.CannonPlane.homeomorphMap line 319
  17. lemma OAI.CannonPlane.complex_map_subsequence line 321
  18. theorem OAI.CannonPlane.pointwise_bounded_homeomorph_subsequence line 352
  19. theorem OAI.CannonPlane.normalized_smooth_qc_subsequence line 393