OAI/Analysis/CircleDomains/Topology/ProjectionJordanCap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A continuous extension of the inverse carries a matched closed Jordan cap into its source cap. The boundary identity prevents crossing the source curve, and a domain point identifies the correct side.

  1. theorem OAI.CircleDomainRigidity.inverse_projection_fiber_on_domain line 14
  2. theorem OAI.CircleDomainRigidity.inverse_projection_matched_cap line 29