OAI/Analysis/CircleDomains/Rigidity/MatchedEndChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Refinement of matched source and target ends

A finer source contour lies on the chosen source side exactly when its matched target contour lies on the corresponding target side. Filling both Jordan contours upgrades boundary containment to strict closed-disk containment.

  1. theorem OAI.CircleDomainRigidity.matched_jordan_disk_subset_iff line 24