OAI/Analysis/CircleDomains/Topology/PhysicalPlaneCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite physical chart in the Euclidean coordinates used for smoothing.

  1. def OAI.CircleDomainRigidity.complexPlaneCoordinates line 12
  2. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_apply line 15
  3. def OAI.CircleDomainRigidity.planeSphere line 18
  4. theorem OAI.CircleDomainRigidity.continuous_planeSphere line 20
  5. def OAI.CircleDomainRigidity.physicalPlaneDomain line 23
  6. theorem OAI.CircleDomainRigidity.isOpen_physicalPlaneDomain line 25
  7. theorem OAI.CircleDomainRigidity.exists_planeSphere_eq line 28
  8. theorem OAI.CircleDomainRigidity.physical_closed_rectangle_of_coordinate_subset line 36
  9. theorem OAI.CircleDomainRigidity.complex_rectangle_diameter_of_coordinate_diameter line 48