OAI/Analysis/CircleDomains/Modulus/HolomorphicStrictNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A holomorphic injection cannot attain a positive lower modulus bound, or any upper modulus bound, in the interior.

  1. lemma OAI.CircleDomainRigidity.holomorphicInjOn_norm_gt line 13
  2. lemma OAI.CircleDomainRigidity.holomorphicInjOn_norm_lt line 32