OAI/Analysis/CircleDomains/Selection/RealSeedPresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real barriers used as the seed already vanish on the anchor neighborhood of infinity. This gives the compact support required by the later generic-level estimates, with the identical quotient coordinate.

  1. def OAI.CircleDomainRigidity.UngatedRealTest.levelPresentation line 19