OAI/Analysis/CircleDomains/Selection/PrincipalInversionGerm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The inversion conjugate of a principal holomorphic exterior map has an analytic germ at zero with derivative one.

  1. def OAI.CircleDomainRigidity.principalInversionGerm line 12
  2. lemma OAI.CircleDomainRigidity.principalInversionGerm_eq line 15
  3. lemma OAI.CircleDomainRigidity.principalInversionGerm_analytic_deriv line 33