OAI/Analysis/CircleDomains/Topology/CompactBandNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Singleton fibers of a compact band graph have uniformly narrow nearby fibers. This gives the local branch ranges used near free points.

  1. theorem OAI.CircleDomainRigidity.exists_open_compact_band_range line 13
  2. theorem OAI.CircleDomainRigidity.exists_narrow_real_band_neighborhood line 30