Theorems · Theorem · complex analysis

Complex.exists_continuousOn_eqOn_exp_comp

∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsSimplyConnected U →
    IsOpen U → ∀ {g : X → ℂ}, ContinuousOn g U → 0 ∉ g '' U → ∃ f, ContinuousOn f U ∧ Set.EqOn (Complex.exp ∘ f) g U

If g : X → ℂ defined on a locally path connected space is continuous on an open simply connected set U and 0 ∉ g '' U, then there exists a continuous branch of log ∘ g on U. More precisely, there exists a function f : X → ℂ continuous on U such that exp (f x) = g x for all x ∈ U.

Defined in

Mathlib.Analysis.Complex.BranchLogRoot

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyPathConnectedSpace