tendsto_atTop — Mathlib

English

For a function u: β → α with β nonempty and a supremum order, Tendsto u to a along atTop is equivalent to: for every ε>0 there exists N such that for all n ≥ N, dist(u(n), a) < ε.

Русский

Для функции u: β → α (β непусто) с полем частичного порядка, сходность u к a вдоль atTop эквивалентна: ∀ ε>0 ∃N: ∀ n ≥ N, dist(u(n), a) < ε.

LaTeX

$$Tendsto u atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε$$

Lean4

theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  (atTop_basis.tendsto_iff nhds_basis_ball).trans <| by simp only [true_and, mem_ball, mem_Ici]

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