OAI/Analysis/CircleDomains/Selection/PeriodDomainValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On the physical domain, the assembled period bands are the actual circle-valued coordinate. Only continuity in the local patch is needed.

  1. theorem OAI.CircleDomainRigidity.circleBandGraph_of_continuousAt line 13
  2. theorem OAI.CircleDomainRigidity.periodBandGraph_on_domain line 34