f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) (f c) ≤ R / R * dist z c
⊢ dist (f z) c ≤ dist z c
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ dist (f z) c ≤ dist z c
have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) c ≤ R / R * dist z c
⊢ R ≠ 0
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) (f c) ≤ R / R * dist z c
⊢ dist (f z) c ≤ dist z c
rwa [hc, div_self, one_mul] at this
no goals
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) c ≤ R / R * dist z c
⊢ R ≠ 0
exact (nonempty_ball.1 ⟨z, hz⟩).ne'
no goals
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ MapsTo f (ball c R) (ball (f c) ?m.43512)
rwa [hc]