OAI/Analysis/CircleDomains/Reflection/HolomorphicBoundaryInjectivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

For an open holomorphic map preserving the strict upper side, interior injectivity forces injectivity also on the real boundary. Thus boundary injectivity need not be supplied as an extra extension assumption.

  1. lemma OAI.CircleDomainRigidity.not_eventually_constant_at_real_boundary line 14
  2. lemma OAI.CircleDomainRigidity.holomorphic_map_nhds_at_real_boundary line 32
  3. lemma OAI.CircleDomainRigidity.holomorphic_injOn_upperClosed line 42