OAI/Analysis/CircleDomains/Topology/SaturatedFrontier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A saturated open set with closed projected closure has its exact projected frontier. This identifies the boundary of the quotient collars.

  1. theorem OAI.CircleDomainRigidity.frontier_image_of_saturated_open line 14