OAI/Analysis/CircleDomains/Rigidity/MaskTopology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Masks away from their retained boundaries

A connected filling cap disjoint from the mask boundary is wholly on one side. Away from that boundary, extending a circle coordinate by zero outside the mask is smooth and its intrinsic differential is exactly the indicated covector.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.connected_set_avoiding_mask_boundary line 22
  2. def OAI.CircleDomainRigidity.FiniteTransfer.maskCircleMap line 34
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.maskCircleMap_eventuallyEq_inside line 38
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.maskCircleMap_eventuallyEq_outside line 44
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_zero line 50
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_maskCircleMap line 55
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_mask_off_frontier line 66
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleWedges_maskCircleMap_eq line 79
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_masks_off_boundaries line 90