OAI/Analysis/CircleDomains/Selection/ExteriorZeroAnchor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed quotient neighborhood of infinity contains the image of a sufficiently far exterior region in the physical sphere.

  1. theorem OAI.CircleDomainRigidity.exists_exterior_in_quotient_neighborhood line 13