OAI/Analysis/CircleDomains/Reflection/RoundExteriorPoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every neighborhood of one finite round hole meets the exterior of all the holes, also when the chosen hole is a point.

  1. theorem OAI.CircleDomainRigidity.exists_exterior_point_near_round_hole line 13