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.instTopologicalSpaceUpperHalfPlane : TopologicalSpace UpperHalfPlane

Equations

• UpperHalfPlane.instTopologicalSpaceUpperHalfPlane = 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.instSecondCountableTopologyUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : SecondCountableTopology UpperHalfPlane

Equations

• UpperHalfPlane.instSecondCountableTopologyUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instT3SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : T3Space UpperHalfPlane

Equations

• UpperHalfPlane.instT3SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instT4SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : T4Space UpperHalfPlane

Equations

• UpperHalfPlane.instT4SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instContractibleSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : ContractibleSpace UpperHalfPlane

Equations

• UpperHalfPlane.instContractibleSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instLocPathConnectedSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : LocPathConnectedSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocPathConnectedSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instNoncompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : NoncompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instNoncompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

instance UpperHalfPlane.instLocallyCompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : LocallyCompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocallyCompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = ⋯

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 | |UpperHalfPlane.re z| ≤ A ∧ B ≤ UpperHalfPlane.im z}

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

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