OAI/Analysis/CircleDomains/Topology/ProjectedPlaneFunction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continue any compact planar test through the actual matched-end projection. This construction does not require the test to be smooth.

  1. theorem OAI.CircleDomainRigidity.sphereFromPlaneFunction_zero_near_infty line 17
  2. def OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction line 41
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction_continuous line 44
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction_hasCompactSupport line 53
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction_zero_off_image line 71
  6. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction_on_image line 87