obtain ⟨R, hR, hf⟩ := exists_cindex_eq_order hp
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)