OAI/Analysis/CircleDomains/Topology/SphereCompactFrontier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Boundary images under an actual open embedding, and the selected boundary of the closed-exterior extension.

  1. lemma OAI.CircleDomainRigidity.sphere_interior_image_of_open_embedding line 13
  2. lemma OAI.CircleDomainRigidity.sphere_frontier_image_of_open_embedding line 30
  3. lemma OAI.CircleDomainRigidity.frontier_closedTerminalCap line 39
  4. lemma OAI.CircleDomainRigidity.frontier_image_of_closed_extension line 46