OAI/Analysis/CircleDomains/Topology/FinitePlaneEmbedding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Openness, injectivity and continuity of the actual finite-plane maps induced by the normalized smooth sphere equivalences.

  1. theorem OAI.CircleDomainRigidity.IsSmoothSphereAt.continuousAt_finite_map line 17
  2. theorem OAI.CircleDomainRigidity.finite_part_image_eq line 29
  3. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.finite_open_embedding line 40