Theorems · Theorem · complex analysis

AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux

∀ {f : ℂ → ℂ} {z₀ : ℂ}, AnalyticAt ℂ f z₀ → (∀ᶠ (z : ℂ) in nhds z₀, f z = f z₀) ∨ nhds (f z₀) ≤ Filter.map f (nhds z₀)

A function f : ℂ → ℂ which is analytic at a point z₀ is either constant in a neighborhood of z₀, or behaves locally like an open function (in the sense that the image of every neighborhood of z₀ is a neighborhood of f z₀, as in isOpenMap_iff_nhds_le). For a function f : E → ℂ the same result holds, see AnalyticAt.eventually_constant_or_nhds_le_map_nhds.

Defined in

Mathlib.Analysis.Complex.OpenMapping

Cited by

1 results in Mathlib

Foundations

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