have e1 : IsCompact (closedBall c r) := isCompact_closedBall _ _
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0