English
If for every ε > 0 there exists r such that outside the ball of radius r, ||f(x)|| < ε, then f tends to 0 along cocompact filter: Tendsto f (cocompact E) (𝓝 0).
Русский
Если для каждого ε > 0 существует радиус r, такой что за пределами шара радиуса r |f(x)| < ε, то f стремится к 0 по фильтру cocompact: Tendsto f (cocompact E) (𝓝 0).
LaTeX
$$$\left(\forall \varepsilon>0, \exists r\in \mathbb{R}, \forall x\,\big(r<\|x\| \Rightarrow \|f(x)\|<\varepsilon\big)\right) \Rightarrow \mathrm{Tendsto}\ f\ (\mathrm{cocompact}\ E)\ (\mathcal{N}\!_0)$$$
Lean4
theorem zero_at_infty_of_norm_le (f : E → F)
(h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε) : Tendsto f (cocompact E) (𝓝 0) :=
by
rw [tendsto_zero_iff_norm_tendsto_zero]
intro s hs
rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]
rw [Metric.mem_nhds_iff] at hs
rcases hs with ⟨ε, hε, hs⟩
rcases h ε hε with ⟨r, hr⟩
use r
intro
aesop
