OAI/Analysis/CircleDomains/Rigidity/MaskBranchCollars.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Disjoint compact boundaries admit smaller closed collars. Coordinate absence on a collar is realized by a constant exterior replacement; present coordinates retain their given local real branches.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_disjoint_closed_collars line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.midpoint_notMem_shiftedLattice line 35
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_mask_branch_collars line 43