OAI/Analysis/CircleDomains/Selection/PhysicalRealCoordinate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A genuine continuous quotient coordinate with its smooth finite-energy physical representative, ready for finite transfer.

  1. structure OAI.CircleDomainRigidity.PhysicalRealCoordinate line 18
  2. theorem OAI.CircleDomainRigidity.physicalRealCoordinate_of_plane_smoothing line 29