OAI/Analysis/CircleDomains/Topology/PrescribedPlaneCoordinate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On a point-complement source the physical representative retains the entire prescribed continuous sphere function, including every dust value. The zero extension used for its derivatives does not change those values.

  1. theorem OAI.CircleDomainRigidity.exists_prescribed_plane_coordinate line 17