tendsto_nhds_iff_lt — Mathlib

English

In the upper topology, Tendsto f l x is characterized by: for every y with y < x, eventually y < f z.

Русский

В верхней топологии стремление f по l к x эквивалентно: для каждого y < x существует момент, после которого y < f(z).

LaTeX

$$$\text{Tendsto } f\, l\ (\mathcal{N} x) \iff \forall y < x, \forall^\infty z \in l, y < f(z)$$$

Lean4

theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
    Filter.Tendsto f l (𝓝 x) ↔ ∀ y < x, ∀ᶠ z in l, y < f z :=
  IsLower.tendsto_nhds_iff_lt (α := αᵒᵈ)

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