OAI/Analysis/CircleDomains/Topology/SphereSliceChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every finite physical point has a chart neighborhood with a concrete inverse Lipschitz bound. This is used only on compact coordinate slices.

  1. theorem OAI.CircleDomainRigidity.exists_sphereSliceChart line 18
  2. theorem OAI.CircleDomainRigidity.finiteCoord_lipschitz_on_compact_chart line 31