OAI/Analysis/CircleDomains/Selection/RealTestCoordinateFamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The final marked set may contain both budget atoms and countably many uncovered ends. The selected coordinates retain their actual boundary bands.

  1. def OAI.CircleDomainRigidity.realTestCoordinateFamily line 18
  2. theorem OAI.CircleDomainRigidity.realTestCoordinateFamily_naturalCompatibility line 38