Topology on the upper half plane

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

instance UpperHalfPlane.instTopologicalSpace : TopologicalSpace UpperHalfPlane

Equations

• UpperHalfPlane.instTopologicalSpace = instTopologicalSpaceSubtype

theorem UpperHalfPlane.openEmbedding_coe : OpenEmbedding UpperHalfPlane.coe

theorem UpperHalfPlane.embedding_coe : Embedding UpperHalfPlane.coe

theorem UpperHalfPlane.continuous_coe : Continuous UpperHalfPlane.coe

theorem UpperHalfPlane.continuous_re : Continuous UpperHalfPlane.re

theorem UpperHalfPlane.continuous_im : Continuous UpperHalfPlane.im

instance UpperHalfPlane.instSecondCountableTopology : SecondCountableTopology UpperHalfPlane

Equations

• UpperHalfPlane.instSecondCountableTopology = ⋯

instance UpperHalfPlane.instT3Space : T3Space UpperHalfPlane

Equations

• UpperHalfPlane.instT3Space = ⋯

instance UpperHalfPlane.instT4Space : T4Space UpperHalfPlane

Equations

• UpperHalfPlane.instT4Space = ⋯

instance UpperHalfPlane.instContractibleSpace : ContractibleSpace UpperHalfPlane

Equations

• UpperHalfPlane.instContractibleSpace = ⋯

instance UpperHalfPlane.instLocPathConnectedSpace : LocPathConnectedSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocPathConnectedSpace = ⋯

instance UpperHalfPlane.instNoncompactSpace : NoncompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instNoncompactSpace = ⋯

instance UpperHalfPlane.instLocallyCompactSpace : LocallyCompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocallyCompactSpace = ⋯

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

• UpperHalfPlane.verticalStrip A B = {z : UpperHalfPlane | |z.re| ≤ A ∧ B ≤ z.im}

theorem UpperHalfPlane.mem_verticalStrip_iff (A : ℝ) (B : ℝ) (z : UpperHalfPlane) : z ∈ UpperHalfPlane.verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im

theorem UpperHalfPlane.verticalStrip_mono {A : ℝ} {B : ℝ} {A' : ℝ} {B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) : UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B'

theorem UpperHalfPlane.verticalStrip_mono_left {A : ℝ} {A' : ℝ} (h : A ≤ A') (B : ℝ) : UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B

theorem UpperHalfPlane.verticalStrip_anti_right (A : ℝ) {B : ℝ} {B' : ℝ} (h : B' ≤ B) : UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A B'

theorem UpperHalfPlane.subset_verticalStrip_of_isCompact {K : Set UpperHalfPlane} (hK : IsCompact K) : ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ UpperHalfPlane.verticalStrip A B

theorem UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip (z : UpperHalfPlane) {N : ℕ} (hn : 0 < N) : ∃ (n : ℤ), ModularGroup.T ^ (↑N * n) • z ∈ UpperHalfPlane.verticalStrip (↑N) z.im

def UpperHalfPlane.ofComplex : PartialHomeomorph ℂ UpperHalfPlane

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

Equations

• UpperHalfPlane.ofComplex = (OpenEmbedding.toPartialHomeomorph UpperHalfPlane.coe UpperHalfPlane.openEmbedding_coe).symm

def UpperHalfPlane.«term↑ₕ_» : Lean.ParserDescr

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

Equations

• UpperHalfPlane.«term↑ₕ_» = Lean.ParserDescr.node `UpperHalfPlane.term↑ₕ_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑ₕ") (Lean.ParserDescr.cat `term 0))

theorem UpperHalfPlane.ofComplex_apply (z : UpperHalfPlane) : ↑UpperHalfPlane.ofComplex ↑z = z

theorem UpperHalfPlane.comp_ofComplex (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : (f ∘ ↑UpperHalfPlane.ofComplex) ↑z = f z