rintro f ⟨i, rfl⟩
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ range F ⊆ 𝓑 U Q
case intro
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
i : ι
⊢ F i ∈ 𝓑 U Q