ring
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε * (2 * Real.pi * r) = 2 * Real.pi * r * ε
no goals