Theorems · Theorem · general topology

Continuous.upperHalfPlaneMk

∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℂ},
  Continuous f → ∀ (hf₀ : ∀ (x : X), 0 < (f x).im), Continuous fun x => { coe := f x, coe_im_pos := ⋯ }

Defined in

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace