OAI/Analysis/CircleDomains/Rigidity/MatchedComponentSides.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Trapping a corresponding component by any retained contour

The source end need only lie inside the chosen contour. Compactness places a sufficiently late source collar there, and the matched side equality places its target collar inside the target contour.

  1. theorem OAI.CircleDomainRigidity.SmoothJordanCore.omitted_point_mem_side line 22
  2. theorem OAI.CircleDomainRigidity.matched_component_subset_retained_side line 35