Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Topology on the upper half plane #

In this file we introduce a TopologicalSpace structure on the upper half plane and provide various instances.

The vertical strip of width A and height B, defined by elements whose real part has absolute value less than or equal to A and imaginary part is at least B.

Equations
Instances For
    theorem UpperHalfPlane.verticalStrip_mono {A : } {B : } {A' : } {B' : } (hA : A A') (hB : B' B) :

    Extend a function on arbitrarily to a function on all of .

    Equations
    Instances For
      theorem UpperHalfPlane.ofComplex_apply_eq_ite (w : ) :
      UpperHalfPlane.ofComplex w = if hw : 0 < w.im then w, hw else Classical.choice
      theorem UpperHalfPlane.comp_ofComplex_of_im_pos (f : UpperHalfPlane) (z : ) (hz : 0 < z.im) :
      (f UpperHalfPlane.ofComplex) z = f z, hz
      theorem UpperHalfPlane.comp_ofComplex_of_im_le_zero (f : UpperHalfPlane) (z : ) (z' : ) (hz : z.im 0) (hz' : z'.im 0) :
      theorem Complex.isConnected_of_upperHalfPlane {s : Set } (hs₁ : {z : | 0 < z.im} s) (hs₂ : s {z : | 0 z.im}) :
      theorem Complex.isConnected_of_lowerHalfPlane {s : Set } (hs₁ : {z : | z.im < 0} s) (hs₂ : s {z : | z.im 0}) :