Theorems · Theorem · complex analysis

Complex.exists_continuousOn_pow_eq

∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsSimplyConnected U →
    IsOpen U →
      ∀ {g : X → ℂ}, ContinuousOn g U → 0 ∉ g '' U → ∀ {n : ℕ}, n ≠ 0 → ∃ f, ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

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

Defined in

Mathlib.Analysis.Complex.BranchLogRoot

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyPathConnectedSpace