tendsto_order_unbounded — Mathlib

English

Given a,b with a below and above, if f maps arbitrary small intervals into a-b neighborhood, then f→a.

Русский

Если существуют окрестности слева и справа от a, и отображение f отправляет малые интервалы в эти окрестности, то f сходится к a.

LaTeX

$$$\\text{tendsto\_order\_unbounded} \\; [OrderTopology\\ α]\\; (f:β→α) \\; (a:α) \\; (x:Filter β) \\; (hu:∃u, a

Lean4

theorem tendsto_order_unbounded [OrderTopology α] {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u) (hl : ∃ l, l < a)
    (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) : Tendsto f x (𝓝 a) :=
  by
  simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
  exact fun l hl u => h l u hl

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