OAI/Analysis/CircleDomains/Topology/CircleRealCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit local real charts of the circle and the open-image theorem for circle embeddings into a real one-manifold.

  1. lemma OAI.CircleDomainRigidity.exists_real_circle_chart line 14
  2. lemma OAI.CircleDomainRigidity.isOpenMap_circle_to_real_manifold line 32