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.instTopologicalSpaceUpperHalfPlane :
TopologicalSpace UpperHalfPlane
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.instSecondCountableTopologyUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
TopologicalSpace.SecondCountableTopology UpperHalfPlane
source
instance UpperHalfPlane.instT3SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
T3Space UpperHalfPlane
source
instance UpperHalfPlane.instT4SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
T4Space UpperHalfPlane
source
instance UpperHalfPlane.instContractibleSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
ContractibleSpace UpperHalfPlane
source
instance UpperHalfPlane.instLocPathConnectedSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
LocPathConnectedSpace UpperHalfPlane
source
instance UpperHalfPlane.instNoncompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
NoncompactSpace UpperHalfPlane
source
instance UpperHalfPlane.instLocallyCompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane :
LocallyCompactSpace UpperHalfPlane