OAI/Analysis/CircleDomains/Topology/ConformalSphericalMetric.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ordinary conformality supplies the metric-conformality predicate for the unchanged spherical background, including the infinity chart.

  1. theorem OAI.CircleDomainRigidity.IsConformalAt.isMetricConformalAt_of_scalar line 13
  2. theorem OAI.CircleDomainRigidity.IsConformalAt.isMetricConformalAt_spherical line 44