OAI/Analysis/CircleDomains/Topology/ClosedGapAvoidance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Closed retained gaps avoid the interiors of the deleted intervals. Their endpoints lie on the enlarged circles, outside the original disks.

  1. theorem OAI.CircleDomainRigidity.closed_gaps_avoid_hole_interiors line 10
  2. theorem OAI.CircleDomainRigidity.closed_gaps_inside line 28