English
Limit to infinity for WithSeminorms: Tendsto u to y0 along atTop is equivalent to, for every i and ε>0, there exists x0 such that for all x≥x0, p_i(u(x)−y0) < ε.
Русский
Предел вдоль бесконечности для WithSeminorms: Tendsto u вдоль atTop к y0 эквивалентно тому, что для каждого i и ε>0 существует x0, такое что для всех x≥x0 выполняется p_i(u(x)−y0) < ε.
LaTeX
$$$hp:\\; WithSeminorms\\ p \\rightarrow (Tendsto\\ u\\ atTop\\ (nhds\\ y_0))\\iff \\forall i,\\forall \\varepsilon>0,\\ exists x_0,\\forall x\\ge x_0,\\ p_i(u(x)-y_0)<\\varepsilon$$$
Lean4
/-- Limit `→ ∞` for `WithSeminorms`. -/
theorem tendsto_nhds_atTop (hp : WithSeminorms p) (u : F → E) (y₀ : E) :
Filter.Tendsto u Filter.atTop (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∃ x₀, ∀ x, x₀ ≤ x → p i (u x - y₀) < ε :=
by
rw [hp.tendsto_nhds u y₀]
exact forall₃_congr fun _ _ _ => Filter.eventually_atTop
