isZeroAtImInfty_iff — Mathlib

English

For a function f : ℍ → α with SeminormedAddGroup structure, IsZeroAtImInfty f is equivalent to: for every ε > 0 there exists A ∈ ℝ such that for all z ∈ ℍ with Im z ≥ A we have ‖f z‖ ≤ ε.

Русский

Для функции f : ℍ → α с полем полей Половинной группы, IsZeroAtImInfty f эквивалентно: для каждого ε > 0 существует A ∈ ℝ такое, что для всех z ∈ ℍ с Im z ≥ A выполняется ‖f(z)‖ ≤ ε.

LaTeX

$$$\text{IsZeroAtImInfty}(f) \iff \forall \varepsilon>0, \exists A\in\mathbb{R}, \forall z\in\mathbb{H}, A \le \operatorname{im}(z) \Rightarrow \|f(z)\| \le \varepsilon$$$

Lean4

theorem isZeroAtImInfty_iff {α : Type*} [SeminormedAddGroup α] {f : ℍ → α} :
    IsZeroAtImInfty f ↔ ∀ ε : ℝ, 0 < ε → ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → ‖f z‖ ≤ ε :=
  (atImInfty_basis.tendsto_iff Metric.nhds_basis_closedBall).trans <| by simp

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