OAI/Analysis/CircleDomains/Rigidity/MaskedStageCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite model carries a retained source collar to a Jordan collar. Exactly the holes inside that image are selected, and the punctured closed region lies in the transported coordinate's smooth mask.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.exists_collar_region line 16