OAI/Analysis/CircleDomains/Topology/QuotientLocalChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A quotient neighborhood whose closure misses the image of infinity has a bounded inverse physical chart. Domain points in it are covered by that chart using the actual domain homeomorphism.

  1. theorem OAI.CircleDomainRigidity.finiteCoord_lipschitz_quotient_neighborhood line 19
  2. theorem OAI.CircleDomainRigidity.quotient_neighborhood_chart_covers line 32