LeanPool.RiemannMappingTheorem.Montel

def UniformlyBoundedOn {ι : Type u_1} (F : ι → ℂ → ℂ) (U : Set ℂ) : Prop

A family F is uniformly bounded on U iff for every compact K ⊆ U there is a single compact Q ⊆ ℂ containing every F i K.

Equations

• UniformlyBoundedOn F U = ∀ K ∈ compacts U, ∃ (Q : Set ℂ), IsCompact Q ∧ ∀ (i : ι), Set.MapsTo (F i) K Q

theorem UniformlyBoundedOn.deriv {ι : Type u_1} {U : Set ℂ} {F : ι → 𝓒 U} (h1 : UniformlyBoundedOn F U) (hU : IsOpen U) (h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U) : UniformlyBoundedOn (_root_.deriv ∘ F) U

theorem UniformlyBoundedOn.equicontinuousOn {ι : Type u_1} {U K : Set ℂ} {F : ι → 𝓒 U} (h1 : UniformlyBoundedOn F U) (hU : IsOpen U) (h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U) (hK : K ∈ compacts U) : EquicontinuousOn F K

theorem uniformlyBoundedOn_𝓑 {U : Set ℂ} {Q : Set ℂ → Set ℂ} (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) : UniformlyBoundedOn Subtype.val U

theorem isCompact_𝓑 {U : Set ℂ} {Q : Set ℂ → Set ℂ} (hU : IsOpen U) (hQ : ∀ K ∈ compacts U, IsCompact (Q K)) : IsCompact (𝓑 U Q)

theorem montel {ι : Type u_1} {U : Set ℂ} {F : ι → 𝓒 U} (hU : IsOpen U) (h1 : UniformlyBoundedOn F U) (h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U) : TotallyBounded (Set.range F)

theorem isCompact_𝓜 {U : Set ℂ} (hU : IsOpen U) : IsCompact (𝓜 U)