OAI/Analysis/CircleDomains/Topology/CompactChartConjugation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Extend a compactly supported deformation in an actual plane chart by identity outside the chart. The support and smoothness are retained.

  1. def OAI.CircleDomainRigidity.chartConjugate line 14
  2. lemma OAI.CircleDomainRigidity.homeomorph_symm_eq_of_fixed line 19
  3. lemma OAI.CircleDomainRigidity.compactChart_maps_source line 23
  4. lemma OAI.CircleDomainRigidity.chartConjugate_eq_off line 32
  5. lemma OAI.CircleDomainRigidity.chartConjugate_left_inv line 41
  6. lemma OAI.CircleDomainRigidity.chartConjugate_continuous line 55
  7. def OAI.CircleDomainRigidity.compactChartHomeomorph line 78
  8. lemma OAI.CircleDomainRigidity.chartConjugate_contDiff line 89
  9. lemma OAI.CircleDomainRigidity.compactChartHomeomorph_image line 110
  10. lemma OAI.CircleDomainRigidity.compactChartHomeomorph_inverse_smooth line 120