Mathlib Map

Theorems · Theorem · number theory

UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty

∀ {α : Type u_1} [inst : SeminormedAddGroup α] {f : UpperHalfPlane → α},
  UpperHalfPlane.IsZeroAtImInfty f → UpperHalfPlane.IsBoundedAtImInfty f
Defined in
Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Cited by
1 results in Mathlib
Foundations
Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CuspFormClass.petersson_bounded_left · cited by 2CuspFormClass.petersson_b…UpperHalfPlane · cited by 626UpperHalfPlaneSeminormedAddGroup · cited by 331SeminormedAddGroupUpperHalfPlane.IsBoundedAtImInfty · cited by 30UpperHalfPlane.IsBoundedA…UpperHalfPlane.IsZeroAtImInfty · cited by 24UpperHalfPlane.IsZeroAtIm…Filter.ZeroAtFilter.boundedAtFilter · cited by 2ZeroAtFilter.boundedAtFil…IsZeroAtImInfty.isBoundedAtIm…CITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.