tendsto_nhdsWithin_nhds — Mathlib

English

Characterization of convergence to b along a restricted domain s using ε-δ control.

Русский

Характеризация сходимости к b вдоль ограниченной области s через ε-δ контроль.

LaTeX

$$Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, dist x a < δ → dist (f x) b < ε$$

Lean4

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

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