OAI/Analysis/CircleDomains/Uniformization/BandLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identifying the band with the lower and upper boundary limits

This connects the compact graph construction to the manuscript's definition of a real coordinate band by liminf and limsup on the physical domain.

  1. theorem OAI.CircleDomainRigidity.mem_clusterGraph_iff_mapClusterPt line 20
  2. theorem OAI.CircleDomainRigidity.intervalFiberHull_clusterGraph_eq_boundary_band line 49