tendsto_nhdsWithin_nhds — Mathlib

English

Tendsto f from nhdsWithin a s to nhds b is equivalent to a similar ε–δ condition with ε > 0.

Русский

Стремление функции через nhdsWithin эквивалентно аналогичному условию ε–δ с ε > 0.

LaTeX

$$$\\mathrm{Tendsto}\,f\\,(\\mathcal{N}[s]a)\\, (\\mathcal{N}b) \\iff \\forall \\varepsilon>0, \\exists \\delta>0, \\forall \\{x\\}, x\\in s \\to \\operatorname{edist}(x,a) < \\delta \\to \\operatorname{edist}(f(x),b) < \\varepsilon$$$

Lean4

theorem tendsto_nhdsWithin_nhds {a b} :
    Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε :=
  by
  rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
  simp only [mem_univ, true_and]

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