OAI/Analysis/CircleDomains/Selection/LocalBandPaidValues.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local real branches may describe a globally defined closed circle level without extending continuously through its cut. The topological crossing is performed in that global level; real values are used only inside the branch neighborhood.

  1. theorem OAI.CircleDomainRigidity.local_band_paid_values line 16