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 = (_ : SecondCountableTopology ↑fun (point : ℂ) => Real.lt 0 point.im)

instance UpperHalfPlane.instT3SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : T3Space UpperHalfPlane

Equations

• UpperHalfPlane.instT3SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : T3Space { point : ℂ // 0 < point.im })

instance UpperHalfPlane.instT4SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : T4Space UpperHalfPlane

Equations

• UpperHalfPlane.instT4SpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : T4Space UpperHalfPlane)

instance UpperHalfPlane.instContractibleSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : ContractibleSpace UpperHalfPlane

Equations

• UpperHalfPlane.instContractibleSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : ContractibleSpace ↑{c : ℂ | 0 < c.im})

instance UpperHalfPlane.instLocPathConnectedSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : LocPathConnectedSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocPathConnectedSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : LocPathConnectedSpace ↑fun (point : ℂ) => Real.lt 0 point.im)

instance UpperHalfPlane.instNoncompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : NoncompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instNoncompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : NoncompactSpace UpperHalfPlane)

instance UpperHalfPlane.instLocallyCompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane : LocallyCompactSpace UpperHalfPlane

Equations

• UpperHalfPlane.instLocallyCompactSpaceUpperHalfPlaneInstTopologicalSpaceUpperHalfPlane = (_ : LocallyCompactSpace UpperHalfPlane)