Commit 2023-06-28 05:06 580093d4

View on Github →

feat: port Analysis.Complex.UpperHalfPlane.Topology (#5530)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

added theorem UpperHalfPlane.continuous_coe

added theorem UpperHalfPlane.continuous_im

added theorem UpperHalfPlane.continuous_re

added theorem UpperHalfPlane.embedding_coe

added theorem UpperHalfPlane.openEmbedding_coe