upper_half_plane): move topology to a new file (#14748)

Commit

3 years ago

refactor(analysis/complex/upper_half_plane): move topology to a new file (#14748) Also add some instances and lemmas about topology on the upper half plane.

Author

urkud

Parents

804afcb0

mathlib 8263a4bf - refactor(analysis/complex/upper_half_plane): move topology to a new file (#14748)

mathlib
8263a4bf - refactor(analysis/complex/upper_half_plane): move topology to a new file (#14748)