OAI/Analysis/CircleDomains/Topology/RetainedCurveImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Schoenflies and open-map side correspondence for one retained source curve. The curve may surround missing source points.

  1. theorem OAI.CircleDomainRigidity.exists_retained_curve_image line 15
  2. theorem OAI.CircleDomainRigidity.matched_end_subset_retained_side line 61