OAI/Analysis/CircleDomains/Topology/BoundaryGlobalInjectivity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two distinct boundary points cannot have the same image when their local open extensions approach the same target side and the original interior map is injective.

  1. lemma OAI.CircleDomainRigidity.injOn_boundary_of_holomorphic_extensions line 13