LeanPool.RiemannMappingTheorem.DerivInj

theorem crucial {U : Set ℂ} {c z₀ : ℂ} {r : ℝ} {f : ℂ → ℂ} (hU : IsOpen U) (hcr : Metric.closedBall c r ⊆ U) (hz₀ : z₀ ∈ Metric.ball c r) (hf : DifferentiableOn ℂ f U) (hfz₀ : f z₀ = 0) (hf'z₀ : deriv f z₀ ≠ 0) (hfz : ∀ z ∈ Metric.closedBall c r, z ≠ z₀ → f z ≠ 0) : cindex c r f = 1

theorem tendsto_uniformly_on_const {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : α → β} [UniformSpace β] {p : Filter ι} {s : Set α} : TendstoUniformlyOn (fun (x : ι) => f) f p s

theorem bla {z₀ : ℂ} {f : ℂ → ℂ} (hf : AnalyticAt ℂ f z₀) (hf' : HasFPowerSeriesAt (deriv f) 0 z₀) : ∀ᶠ (z : ℂ) in nhds z₀, f z = f z₀

theorem two_le_order_of_deriv_eq_zero {z₀ : ℂ} {g : ℂ → ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} (hgp : HasFPowerSeriesAt g p z₀) (hp : p ≠ 0) (hg : g z₀ = 0) (hg' : deriv g z₀ = 0) : 2 ≤ p.order

theorem tendsto_uniformly_on_add_const {U : Set ℂ} {g : ℂ → ℂ} : TendstoUniformlyOn (fun (ε z : ℂ) => g z + ε) g (nhdsWithin 0 {0}ᶜ) U

theorem deriv_ne_zero_of_inj_aux {U : Set ℂ} {z₀ : ℂ} {g : ℂ → ℂ} (hU : IsOpen U) (hg : DifferentiableOn ℂ g U) (hi : Set.InjOn g U) (hz₀ : z₀ ∈ U) (hgz₀ : g z₀ = 0) : deriv g z₀ ≠ 0

theorem deriv_ne_zero_of_inj {U : Set ℂ} {z₀ : ℂ} {f : ℂ → ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hi : Set.InjOn f U) (hz₀ : z₀ ∈ U) : deriv f z₀ ≠ 0