OAI/Analysis/CircleDomains/Selection/SmallAnchoredCoordinateFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the countable real-coordinate family with arbitrarily small anchored plateaus at every end outside its countable marked set.

  1. theorem OAI.CircleDomainRigidity.exists_small_anchored_coordinates line 19