Montel's theorem

A family of holomorphic maps which is bounded uniformly on each compact subset of its domain is equicontinuous. For finite-dimensional targets it has compact closure in the compact-open topology. Compactness is supplied by Mathlib's Arzelà–Ascoli theorem.

theorem CarlsonFunctions.SeveralComplexVariables.equicontinuous_of_holomorphic_bounded_on_compacts {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : TopologicalSpace.Opens (ι → ℂ)} {S : Set (HolomorphicMap U F)} (hb : ∀ K ⊆ ↑U, IsCompact K → ∃ (M : ℝ), ∀ f ∈ S, ∀ z ∈ K, ‖openExtension U (↑f) z‖ ≤ M) : Equicontinuous fun (f : ↑S) => ⇑↑↑f

Compact-local bounds on a holomorphic family give equicontinuity. Banach targets are allowed here; finite dimensionality is needed only for compactness in Montel's theorem.

theorem CarlsonFunctions.SeveralComplexVariables.isCompact_closure_of_holomorphic_bounded_on_compacts {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [FiniteDimensional ℂ F] {U : TopologicalSpace.Opens (ι → ℂ)} {S : Set (HolomorphicMap U F)} (hb : ∀ K ⊆ ↑U, IsCompact K → ∃ (M : ℝ), ∀ f ∈ S, ∀ z ∈ K, ‖openExtension U (↑f) z‖ ≤ M) : IsCompact (closure S)

Montel's theorem. A compact-locally bounded family of holomorphic maps into a finite-dimensional complex normed space has compact closure in the compact-open topology.