Images of open simply connected sets under injective holomorphic maps

A holomorphic map that is injective on an open set Ω ⊆ ℂ carries Ω to an open set, and carries a simply connected Ω to a simply connected set. Both facts are used by the Riemann mapping theorem, where the image of an extremal map has to be recognized as a domain of the same kind as the original.

The argument

Openness is the open mapping theorem. It is local, so it needs no connectivity hypothesis on Ω: around each point of Ω sits a ball on which g is analytic and — being injective — nonconstant, and Mathlib.Analysis.Complex.OpenMapping opens that ball.

Simple connectivity is then purely topological, and Mathlib supplies it: injectivity and continuity make Ω.domRestrict g an injective continuous map, openness makes it an open map, hence a topological embedding, and Topology.IsEmbedding.isSimplyConnected_image transports simple connectivity across an embedding. Holomorphy enters only through the open mapping theorem; there is no separate homotopy argument here.

Main statements

• TauCeti.isOpen_image_of_differentiableOn_of_injOn — the image of an open set is open.
• TauCeti.isSimplyConnected_image_of_differentiableOn_of_injOn — the image of an open simply connected set is simply connected.

Coordination with upstream Mathlib

The Riemann mapping theorem is being formalized upstream at mathlib4#33505, which proves the L0–L3 prerequisites internally as private lemmas. The declarations here are an explicitly temporary shim: delete them and refactor downstream consumers onto the exported Mathlib versions once those land.

References

• L. Ahlfors, Complex Analysis, Ch. 4 §3.4 (the open mapping theorem).

theorem TauCeti.isOpen_image_of_differentiableOn_of_injOn {Ω : Set ℂ} {g : ℂ → ℂ} (hΩo : IsOpen Ω) (hgd : DifferentiableOn ℂ g Ω) (hgi : Set.InjOn g Ω) : IsOpen (g '' Ω)

The image of an open set under an injective holomorphic map is open. No connectivity hypothesis is needed: openness is local, and on a small ball around any point of Ω the map is analytic and nonconstant, so the open mapping theorem applies there.

theorem TauCeti.isOpenMap_restrict_of_differentiableOn_of_injOn {Ω : Set ℂ} {g : ℂ → ℂ} (hΩo : IsOpen Ω) (hgd : DifferentiableOn ℂ g Ω) (hgi : Set.InjOn g Ω) : IsOpenMap (Ω.domRestrict g)

Restricted to its open domain, an injective holomorphic map is an open map into ℂ: an open subset of the subtype ↥Ω is Ω met with an open set, and the image of that is open by TauCeti.isOpen_image_of_differentiableOn_of_injOn.

theorem TauCeti.isSimplyConnected_image_of_differentiableOn_of_injOn {Ω : Set ℂ} {g : ℂ → ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hgd : DifferentiableOn ℂ g Ω) (hgi : Set.InjOn g Ω) : IsSimplyConnected (g '' Ω)

Injective holomorphic maps preserve simple connectivity. The image of an open simply connected set under a holomorphic map injective on it is again simply connected.

The mathematical content beyond openness is Mathlib's Topology.IsEmbedding.isSimplyConnected_image: the restriction of g to Ω is a topological embedding, because it is continuous, injective, and open.

@[deprecated TauCeti.isOpen_image_of_differentiableOn_of_injOn (since := "2026-07-29")]

theorem TauCeti.isOpen_image_of_injOn {Ω : Set ℂ} {g : ℂ → ℂ} (hΩo : IsOpen Ω) (hgd : DifferentiableOn ℂ g Ω) (hgi : Set.InjOn g Ω) : IsOpen (g '' Ω)

Deprecated compatibility alias for the old name, which named only the injectivity hypothesis.

@[deprecated TauCeti.isSimplyConnected_image_of_differentiableOn_of_injOn (since := "2026-07-29")]

theorem TauCeti.isSimplyConnected_image_of_injOn {Ω : Set ℂ} {g : ℂ → ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hgd : DifferentiableOn ℂ g Ω) (hgi : Set.InjOn g Ω) : IsSimplyConnected (g '' Ω)

Deprecated compatibility alias for the old name, which named only the injectivity hypothesis.