OAI/Analysis/CircleDomains/Rigidity/MatchedDiskDomainGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual matched disks are disjoint from the source and target plane domains. All complementary points lie in one bounded disk.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.source_disjoint_domain line 16
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.target_disjoint_image line 24
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.finite_domain_exterior_radius line 42