OAI/Analysis/CircleDomains/Rigidity/MatchedConformalEnds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Matched Jordan ends for a fixed conformal equivalence, independently of the finite-model representation used to construct that equivalence.

  1. structure OAI.CircleDomainRigidity.MatchedConformalEnds line 14
  2. theorem OAI.CircleDomainRigidity.exists_matched_conformal_ends line 27
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.front_source line 39
  4. structure OAI.CircleDomainRigidity.MatchedConformalEnds.EndAt line 43
  5. def OAI.CircleDomainRigidity.MatchedConformalEnds.endAt line 54
  6. def OAI.CircleDomainRigidity.MatchedConformalEnds.projection line 61
  7. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.projection_on_image line 66
  8. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.projection_outside line 70
  9. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.EndAt.target_nested line 78
  10. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.EndAt.source_in_cap line 84
  11. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.EndAt.projection_in_cap line 96
  12. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.projection_continuous line 113