OAI/Analysis/CircleDomains/Transfer/ModelPairWorkingError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Outside the actual changed horizontal support, only the vertical error remains in the selected two-coordinate source map.

  1. theorem OAI.CircleDomainRigidity.planePair_same_first_norm line 15
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_pair_error_outside_support line 25