OAI/Analysis/CircleDomains/Rigidity/MatchedCommonPoints.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The common point set uses the full matched component family. The single unused-code center may be omitted during local compression and restored at the end, since a singleton has null scalar image.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.commonPointPlane line 17
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.commonPointPlane_singletons line 20
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.commonPoint_gap line 31
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.commonPoint_prefix_avoidance line 43