OAI/Analysis/CircleDomains/Topology/SphereChartInverseControl.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local inverse Lipschitz control for the actual fixed finite sphere chart. The chosen linear coordinates need not be orthonormal.

  1. theorem OAI.CircleDomainRigidity.linear_stereo_inverse_control line 14
  2. theorem OAI.CircleDomainRigidity.finite_sphere_chart_inverse_control line 39