OAI/Analysis/CircleDomains/Topology/DiskFractionalMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The elementary disk fractional transformations used to improve an omitted-value extremal embedding.

  1. def OAI.CircleDomainRigidity.diskFractionalMap line 12
  2. lemma OAI.CircleDomainRigidity.diskFractionalMap_denom_ne_zero line 14
  3. lemma OAI.CircleDomainRigidity.diskFractionalMap_norm_identity line 24
  4. lemma OAI.CircleDomainRigidity.diskFractionalMap_mem_ball line 31
  5. lemma OAI.CircleDomainRigidity.diskFractionalMap_hasDerivAt line 41
  6. lemma OAI.CircleDomainRigidity.diskFractionalMap_injective line 52
  7. lemma OAI.CircleDomainRigidity.diskFractionalMap_self line 65
  8. lemma OAI.CircleDomainRigidity.diskFractionalMap_zero line 68