English
For a family p of seminorms, Tendsto(u,f,nhds y0) is equivalent to the pointwise condition: for every i and every ε>0, p_i(u(x)−y0) < ε eventually along f.
Русский
Для семейства семинорм p: Tendsto(u,f,nhds y0) эквивалентно тому, что для каждого i и ε>0 происходят неуклонные приближения p_i(u(x)−y0) < ε вдоль f.
LaTeX
$$$hp:\\; WithSeminorms\\ p \\Rightarrow\\ (Tendsto\\ u\\ f\\ (nhds\\ y_0))\\iff\\forall i,\\forall \\varepsilon>0,\\ Eventually\\ x\\in f,\\ p_i(u(x)-y_0) < \\varepsilon$$$
Lean4
/-- Convergence along filters for `WithSeminorms`. -/
theorem tendsto_nhds (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
Filter.Tendsto u f (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∀ᶠ x in f, p i (u x - y₀) < ε :=
by
rw [hp.tendsto_nhds' u y₀]
exact
⟨fun h i => by simpa only [Finset.sup_singleton] using h { i }, fun h s ε hε =>
(s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩
