OAI/Analysis/CircleDomains/Topology/MarkedBranchNeighborhoods.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common neighborhoods of marked points retain the very branches used to define their band endpoints. The local limiting oscillation is then exactly the selected width, including after intersecting all patches.

  1. theorem OAI.CircleDomainRigidity.exists_marked_branch_neighborhoods line 15