Commit 2024-08-26 10:46 7f1ee42d

View on Github →

feat: add lemmas for ofComplex evaluations outside UpperHalfPlane (#16005) This is useful in many places to remove (hz : 0 < z.im) hypotheses.

Estimated changes

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

modified theorem UpperHalfPlane.comp_ofComplex

added theorem UpperHalfPlane.comp_ofComplex_of_im_le_zero

added theorem UpperHalfPlane.comp_ofComplex_of_im_pos

added theorem UpperHalfPlane.ofComplex_apply_eq_ite

added theorem UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos

added theorem UpperHalfPlane.ofComplex_apply_of_im_nonpos