tendsto_order — Mathlib

English

For a function f: β → α, Tendsto f x (nhds a) is equivalent to the two-sided convergence criterion: for all a'<a and a'>a, the function eventually stays between a' and a.

Русский

Для функции f: β → α, сходится f в x к a тогда и только тогда, когда для каждой нижней границы a'<a и верхней границы a'>a, значения f бдят пределы.

LaTeX

$$$\\mathrm{Tendsto}(f,x,nhds(a)) \\iff (\\forall a'a, \\forall^{\\infty} b\\in x, f(b)

Lean4

theorem tendsto_order [OrderTopology α] {f : β → α} {a : α} {x : Filter β} :
    Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a' := by
  simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]; rfl

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