tendsto_atTop' — Mathlib

English

A variant of tendsto_atTop using strict inequality n > N instead of n ≥ N.

Русский

Вариант tendsto_atTop с нестрогим неравенством n > N вместо n ≥ N.

LaTeX

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

Lean4

/-- A variant of `tendsto_atTop` that
uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`
-/
theorem tendsto_atTop' [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε :=
  (atTop_basis_Ioi.tendsto_iff nhds_basis_ball).trans <| by simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball]

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