OAI/Analysis/CircleDomains/Rigidity/MatchedDiskNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper control of the actual selected field on circles shrinking to an indexed source disk, including point-to-disk matches.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedPlane_near_indexed_disk line 16