OAI/Analysis/CircleDomains/Modulus/LevelBarrierRebase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Earlier-law constraints change the base-code space, but do not change the geometric barrier problem. Rebase its actual coordinate and size.

  1. def OAI.CircleDomainRigidity.CompatibleLevelBarrier.rebase line 20
  2. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.controlledSize_rebase line 58