OAI/Analysis/CircleDomains/Topology/CountableBandNeighborhoods.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The singleton band at a free point supplies a narrow branch neighborhood. Second countability extracts the countable family used in the local tag null-trace argument.

  1. theorem OAI.CircleDomainRigidity.countable_narrow_real_band_cover line 17
  2. theorem OAI.CircleDomainRigidity.circle_null_image_of_countable_local_traces line 51