tendsto_nhds' — Mathlib

English

A simp lemma form of tendsto_nhds': the same convergence criterion but simplified via Finset singleton handling.

Русский

Упрощённая форма tendsto_nhds': та же критерий сходимости, но через обработку единичного множества в финсетах.

LaTeX

$$$hp:\\; WithSeminorms\\ p\\Rightarrow\\ (tendsto\\ u\\ f\\ (nhds\\ y_0))\\iff \\forall (s: Finset\\ ι) (ε>0),\\ Todo$$

Lean4

/-- Convergence along filters for `WithSeminorms`.

Variant with `Finset.sup`. -/
theorem tendsto_nhds' (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
    Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε), 0 < ε → ∀ᶠ x in f, s.sup p (u x - y₀) < ε := by
  simp [hp.hasBasis_ball.tendsto_right_iff]

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