OAI/Analysis/CircleDomains/Transfer/SmallImageDustContours.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth inner contours can be selected where the two actual compact source coordinates remain uniformly close to a single dust trace.

  1. theorem OAI.CircleDomainRigidity.exists_small_image_dust_contours line 15