isBoundedAt_infty_iff — Mathlib

English

Let f be a function on the upper half-plane with weight k. Then f is bounded at the cusp ∞ if and only if it is bounded at ∞ in the transformed sense.

Русский

Пусть f — функция на верхней полуплоскости с весом k. Тогда она ограничена в точке бесконечности ∞ тогда и только тогда, когда она ограничена в бесконечности после подходящих преобразований.

LaTeX

$$$\mathrm{IsBoundedAt}(\infty,f,k) \iff \mathrm{IsBoundedAtImInfty}(f)$$$

Lean4

theorem isBoundedAt_infty_iff : IsBoundedAt ∞ f k ↔ IsBoundedAtImInfty f :=
  ⟨fun h ↦ by simpa using h 1 (by simp), fun h _ hg ↦ h.slash _ (smul_infty_eq_self_iff.mp hg)⟩

Похожие утверждения