OAI/Analysis/CircleDomains/Topology/FreeBandNeighborhoods.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Zero band budget produces the actual unique trace, and narrow neighborhoods can be chosen with closure in a prescribed chart region.

  1. theorem OAI.CircleDomainRigidity.real_band_fiber_eq_trace_of_zero_width line 15
  2. theorem OAI.CircleDomainRigidity.exists_narrow_real_band_neighborhood_closure line 33
  3. theorem OAI.CircleDomainRigidity.countable_narrow_real_band_cover_closure line 50