OAI/Analysis/CircleDomains/Rigidity/InnerPeriodMask.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An integration curve strictly inside the outer collar admits an enclosing closed period mask still strictly inside that collar. Thus the centered disk coordinate is needed only on its genuine open disk, while the integration curve lies in the interior of the physical mask.

  1. theorem OAI.CircleDomainRigidity.RegularJordanInwardCollar.exists_inner_period_mask line 19