tendsto_nhds_nhds — Mathlib

English

Limit behavior of f at a with respect to nhds of b is captured by an ε-δ condition.

Русский

Предел f в точке a с точки зрения окрестностей b описывается через ε-δ условие.

LaTeX

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

Lean4

theorem tendsto_nhds_nhds [PseudoMetricSpace β] {f : α → β} {a b} :
    Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) b < ε :=
  nhds_basis_ball.tendsto_iff nhds_basis_ball

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