OAI/Analysis/CircleDomains/Topology/ClosedComponentCorrespondence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A closed correspondence on the full spheres. On the domain it is the conformal map; over a complementary component its fiber is the whole matching component. This includes disk-to-point and point-to-disk matches, where a continuous single-valued extension need not exist.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.relationStage line 17
  2. def OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation line 21
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.relationStage_iff line 23
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_closed line 37
  5. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_graph line 51
  6. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_on_domain line 66
  7. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_source_fiber line 74
  8. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_target_fiber line 101