Documentation
SpherePacking
.
ForMathlib
.
FunctionsBoundedAtInfty
Search
return to top
source
Imports
Init
Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Imported by
isBoundedAtImInfty_neg_iff
source
theorem
isBoundedAtImInfty_neg_iff
(
f
:
UpperHalfPlane
→
ℂ
)
:
UpperHalfPlane.IsBoundedAtImInfty
(
-
f
)
↔
UpperHalfPlane.IsBoundedAtImInfty
f