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.

source
instance UpperHalfPlane.instTopologicalSpace :
TopologicalSpace UpperHalfPlane
Equations
source
theorem UpperHalfPlane.openEmbedding_coe :
OpenEmbedding UpperHalfPlane.coe
source
theorem UpperHalfPlane.embedding_coe :
Embedding UpperHalfPlane.coe
source
theorem UpperHalfPlane.continuous_coe :
Continuous UpperHalfPlane.coe
source
theorem UpperHalfPlane.continuous_re :
Continuous UpperHalfPlane.re
source
theorem UpperHalfPlane.continuous_im :
Continuous UpperHalfPlane.im
source
instance UpperHalfPlane.instSecondCountableTopology :
SecondCountableTopology UpperHalfPlane
Equations
source
instance UpperHalfPlane.instT3Space :
T3Space UpperHalfPlane
Equations
source
instance UpperHalfPlane.instT4Space :
T4Space UpperHalfPlane
Equations
source
instance UpperHalfPlane.instContractibleSpace :
ContractibleSpace UpperHalfPlane
Equations
source
instance UpperHalfPlane.instLocPathConnectedSpace :
LocPathConnectedSpace UpperHalfPlane
Equations
source
instance UpperHalfPlane.instNoncompactSpace :
NoncompactSpace UpperHalfPlane
Equations
source
instance UpperHalfPlane.instLocallyCompactSpace :
LocallyCompactSpace UpperHalfPlane
Equations
source
def UpperHalfPlane.verticalStrip (A : ℝ) (B : ℝ) :
Set UpperHalfPlane

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
    source
    theorem UpperHalfPlane.mem_verticalStrip_iff (A : ℝ) (B : ℝ) (z : UpperHalfPlane) :
    z ∈ UpperHalfPlane.verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im
    source
    theorem UpperHalfPlane.verticalStrip_mono {A : ℝ} {B : ℝ} {A' : ℝ} {B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) :
    UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B'
    source
    theorem UpperHalfPlane.verticalStrip_mono_left {A : ℝ} {A' : ℝ} (h : A ≤ A') (B : ℝ) :
    UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B
    source
    theorem UpperHalfPlane.verticalStrip_anti_right (A : ℝ) {B : ℝ} {B' : ℝ} (h : B' ≤ B) :
    UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A B'
    source
    theorem UpperHalfPlane.subset_verticalStrip_of_isCompact {K : Set UpperHalfPlane} (hK : IsCompact K) :
    ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ UpperHalfPlane.verticalStrip A B
    source
    theorem UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip (z : UpperHalfPlane) {N : ℕ} (hn : 0 < N) :
    ∃ (n : ℤ), ModularGroup.T ^ (↑N * n) • z ∈ UpperHalfPlane.verticalStrip (↑N) z.im
    source
    def UpperHalfPlane.ofComplex :
    PartialHomeomorph ℂ UpperHalfPlane

    A continuous section ℂ → ℍ of the natural inclusion map, bundled as a PartialHomeomorph.

    Equations
    Instances For
      source
      def UpperHalfPlane.«term↑ₕ_» :
      Lean.ParserDescr

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

      Equations
      Instances For
        source
        theorem UpperHalfPlane.ofComplex_apply (z : UpperHalfPlane) :
        ↑UpperHalfPlane.ofComplex ↑z = z
        source
        theorem UpperHalfPlane.ofComplex_apply_eq_ite (w : ℂ) :
        ↑UpperHalfPlane.ofComplex w = if hw : 0 < w.im then ⟨w, hw⟩ else Classical.choice ⋯
        source
        theorem UpperHalfPlane.ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) :
        ↑UpperHalfPlane.ofComplex w = Classical.choice ⋯
        source
        theorem UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos {w : ℂ} {w' : ℂ} (hw : w.im ≤ 0) (hw' : w'.im ≤ 0) :
        ↑UpperHalfPlane.ofComplex w = ↑UpperHalfPlane.ofComplex w'
        source
        theorem UpperHalfPlane.comp_ofComplex (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) :
        (f ∘ ↑UpperHalfPlane.ofComplex) ↑z = f z
        source
        theorem UpperHalfPlane.comp_ofComplex_of_im_pos (f : UpperHalfPlane → ℂ) (z : ℂ) (hz : 0 < z.im) :
        (f ∘ ↑UpperHalfPlane.ofComplex) z = f ⟨z, hz⟩
        source
        theorem UpperHalfPlane.comp_ofComplex_of_im_le_zero (f : UpperHalfPlane → ℂ) (z : ℂ) (z' : ℂ) (hz : z.im ≤ 0) (hz' : z'.im ≤ 0) :
        (f ∘ ↑UpperHalfPlane.ofComplex) z = (f ∘ ↑UpperHalfPlane.ofComplex) z'
        source
        theorem Complex.isConnected_of_upperHalfPlane {s : Set ℂ} (hs₁ : {z : ℂ | 0 < z.im} ⊆ s) (hs₂ : s ⊆ {z : ℂ | 0 ≤ z.im}) :
        IsConnected s
        source
        theorem Complex.isConnected_of_lowerHalfPlane {s : Set ℂ} (hs₁ : {z : ℂ | z.im < 0} ⊆ s) (hs₂ : s ⊆ {z : ℂ | z.im ≤ 0}) :
        IsConnected s