Topology on the upper half plane #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[protected, instance]

noncomputable def upper_half_plane.topological_space :

topological_space upper_half_plane

Equations

upper_half_plane.topological_space = subtype.topological_space

source

theorem upper_half_plane.open_embedding_coe :

open_embedding coe

source

theorem upper_half_plane.embedding_coe :

embedding coe

source

theorem upper_half_plane.continuous_coe :

continuous coe

source

theorem upper_half_plane.continuous_re :

continuous upper_half_plane.re

source

theorem upper_half_plane.continuous_im :

continuous upper_half_plane.im

source

@[protected, instance]

def upper_half_plane.topological_space.second_countable_topology :

topological_space.second_countable_topology upper_half_plane

source

@[protected, instance]

def upper_half_plane.t3_space :

t3_space upper_half_plane

source

@[protected, instance]

def upper_half_plane.normal_space :

normal_space upper_half_plane

source

@[protected, instance]

def upper_half_plane.contractible_space :

contractible_space upper_half_plane

source

@[protected, instance]

def upper_half_plane.loc_path_connected_space :

loc_path_connected_space upper_half_plane

source

@[protected, instance]

def upper_half_plane.noncompact_space :

noncompact_space upper_half_plane

source

@[protected, instance]

def upper_half_plane.locally_compact_space :

locally_compact_space upper_half_plane