Commit 2023-06-28 10:21 ff61283e

View on Github →

feat: port Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (#5531)

Estimated changes

Modified Mathlib.lean

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

added def UpperHalfPlane.IsBoundedAtImInfty

added def UpperHalfPlane.IsZeroAtImInfty

added def UpperHalfPlane.atImInfty

added theorem UpperHalfPlane.atImInfty_basis

added theorem UpperHalfPlane.atImInfty_mem

added def UpperHalfPlane.boundedAtImInftySubalgebra

added theorem UpperHalfPlane.bounded_mem

added def UpperHalfPlane.zeroAtImInftySubmodule

added theorem UpperHalfPlane.zero_at_im_infty

added theorem UpperHalfPlane.zero_form_isBoundedAtImInfty