OAI/Analysis/CircleDomains/Sobolev/PrincipalCircleAreaLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The principal exterior germ determines the limiting signed image area.

  1. theorem OAI.CircleDomainRigidity.principal_circle_area_limit line 11