Functions Bounded at Infinity

Auxiliary lemmas about functions bounded at the cusps.

theorem isBoundedAtImInfty_neg_iff (f : UpperHalfPlane → ℂ) : UpperHalfPlane.IsBoundedAtImInfty (-f) ↔ UpperHalfPlane.IsBoundedAtImInfty f