Theorems · Theorem · complex analysis

DiffContOnCl.ball_subset_image_closedBall

∀ {f : ℂ → ℂ} {z₀ : ℂ} {ε r : ℝ},
  DiffContOnCl ℂ f (Metric.ball z₀ r) →
    0 < r →
      (∀ z ∈ Metric.sphere z₀ r, ε ≤ ‖f z - f z₀‖) →
        (∃ᶠ (z : ℂ) in nhds z₀, f z ≠ f z₀) → Metric.ball (f z₀) (ε / 2) ⊆ f '' Metric.closedBall z₀ r

If the modulus of a holomorphic function f is bounded below by ε on a circle, then its range contains a disk of radius ε / 2.

Defined in

Mathlib.Analysis.Complex.OpenMapping

Cited by

1 results in Mathlib

Foundations

Depth 293 from the axioms · uses propext, Classical.choice, Quot.sound