OAI/Analysis/CircleDomains/Topology/InnerCollarCoordinate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive collar slices lie inside the punctured coordinate disk. The outer boundary is used only as a limit, so it need not lie in the open coordinate domain.

  1. theorem OAI.CircleDomainRigidity.orientedParameter_surjective line 13
  2. theorem OAI.CircleDomainRigidity.OrderedCollarLift.inner_frontier_punctured line 20