OAI/Analysis/CircleDomains/Rigidity/NormalizedRigidityFromTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite flux and the published exterior area theorem force a principally normalized map to be the identity.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.normalized_identity_of_trace line 18