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 = ⋯