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

theorem IsBoundedAtImInfty.neg (f : UpperHalfPlane → ℂ) : UpperHalfPlane.IsBoundedAtImInfty f → UpperHalfPlane.IsBoundedAtImInfty (-f)

Alias of the reverse direction of isBoundedAtImInfty_neg_iff.