OAI/Analysis/CircleDomains/Modulus/NormalFamilyInputs.lean

Classical normal-family inputs

The two propositions are classical consequences of Ahlfors, Complex Analysis, third edition (1979):

• Chapter 5, Theorem 15, p. 224 (Montel compactness), in its diagonal exhaustion form, with the varying-domain convention of Chapter 5, Section 1.1, pp. 176–177. Holomorphy of the locally uniform limit follows from Mathlib.
• Chapter 5, Theorem 2, p. 178 (Hurwitz), applied to injective maps as in Chapter 6, Section 1.1, p. 231. Discarding finitely many initial terms gives the eventually holomorphic and injective formulation.