OAI/Analysis/CircleDomains/Topology/CompactBandCrossing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact graph with nonempty interval fibers has the intermediate value property along connected sets. This supplies the sign separation argument for the closed coordinate bands, including at dust points.

  1. theorem OAI.CircleDomainRigidity.compact_band_crossing line 15
  2. theorem OAI.CircleDomainRigidity.real_band_graph_crossing line 46