English
If f belongs to the class of ZeroAtInftyContinuousMap, then for every ε > 0 there exists r such that for all x with ||x|| > r, we have ||f(x)|| < ε.
Русский
Если функция f принадлежит классу ZeroAtInftyContinuousMap, то для каждого ε > 0 существует радиус r > 0 such that при ||x|| > r выполняется ||f(x)|| < ε.
LaTeX
$$$\forall \varepsilon>0,\; \exists r\in \mathbb{R},\; \forall x, \ r<\|x\| \Rightarrow \|f(x)\|<\varepsilon$$$
Lean4
theorem norm_le (f : 𝓕) (ε : ℝ) (hε : 0 < ε) : ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε :=
by
have h := zero_at_infty f
rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h
specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)
rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
use r
intro x hr'
suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by simp_all
apply hr
simp_all
