OAI/Analysis/CircleDomains/Topology/HalfPlaneDisk.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The Cayley coordinate for compactifying the upper half-plane rays.

  1. def OAI.CircleDomainRigidity.halfPlaneDisk line 13
  2. theorem OAI.CircleDomainRigidity.halfPlaneDisk_den_ne_zero line 15
  3. theorem OAI.CircleDomainRigidity.halfPlaneDisk_normSq line 21
  4. theorem OAI.CircleDomainRigidity.halfPlaneDisk_norm_le line 27
  5. theorem OAI.CircleDomainRigidity.halfPlaneDisk_norm_lt line 35
  6. theorem OAI.CircleDomainRigidity.halfPlaneDisk_norm_eq line 43
  7. theorem OAI.CircleDomainRigidity.continuousOn_halfPlaneDisk line 51
  8. theorem OAI.CircleDomainRigidity.halfPlaneDisk_injOn line 55
  9. theorem OAI.CircleDomainRigidity.halfPlaneDisk_sub_one line 65
  10. theorem OAI.CircleDomainRigidity.halfPlaneDisk_ne_one line 71
  11. theorem OAI.CircleDomainRigidity.halfPlaneDisk_dist_one_le line 79