OAI/Analysis/CircleDomains/Reflection/CayleyBoundaryOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The real boundary of the half-plane is sent monotonically to the positively oriented circle cut at the point at infinity.

  1. def OAI.CircleDomainRigidity.cayleyBoundaryAngle line 17
  2. theorem OAI.CircleDomainRigidity.cayleyBoundary_norm line 19
  3. theorem OAI.CircleDomainRigidity.cayleyBoundary_ne_one line 22
  4. theorem OAI.CircleDomainRigidity.continuous_cayleyBoundaryAngle line 25
  5. theorem OAI.CircleDomainRigidity.cayleyBoundaryAngle_injective line 45
  6. theorem OAI.CircleDomainRigidity.cayleyBoundaryAngle_zero line 51
  7. theorem OAI.CircleDomainRigidity.cayleyBoundaryAngle_one line 59
  8. theorem OAI.CircleDomainRigidity.strictMono_cayleyBoundaryAngle line 74
  9. theorem OAI.CircleDomainRigidity.cayleyBoundary_mem_closingArc line 81