OAI/Analysis/CircleDomains/Transfer/ChartFiberConcentration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Concentrating Euclidean supports control selected values through a closed sphere projection. No comparison of chart and sphere metrics is needed.

  1. theorem OAI.CircleDomainRigidity.concentrated_fiber_values_in_chart line 13
  2. theorem OAI.CircleDomainRigidity.priority_continuousAt_singleton_fiber_in_chart line 49