OAI/Analysis/CircleDomains/Rigidity/TraceBandLevel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At a point with a genuine limiting real trace, the entire circle band is the single projected trace value.

  1. theorem OAI.CircleDomainRigidity.circleBandGraph_of_trace line 13