OAI/Analysis/CircleDomains/Selection/LocalBandTransitions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integer changes of local sheet preserve the actual interval-band level graph. Eventual equality is enough: values outside the patch do not enter its boundary band.

  1. theorem OAI.CircleDomainRigidity.clusterGraph_add_const_of_eventuallyEq line 15
  2. theorem OAI.CircleDomainRigidity.intervalBand_add_const_of_eventuallyEq line 30
  3. theorem OAI.CircleDomainRigidity.circleBand_fiber_eq_of_eventually_add_int line 50