OAI/Analysis/CircleDomains/Modulus/BarrierRebase.lean

GitHub source file

3 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.PhysicalRealCoordinate.rebase line 19
  2. def OAI.CircleDomainRigidity.CompatibleRealBarrier.rebase line 34
  3. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.controlledSize_rebase line 72