tendsto_nhds_iff_not_le — Mathlib

English

For a function into a space with the lower topology, Tendsto to nhds x is equivalent to eventual not-le statements: for every y not ≤ x, eventually not (y ≤ f z).

Русский

Для функции в пространство с нижней топологией, соответсвие сходства к nhds x эквивалентно конечным условиям: для каждого y, не меньшего x, по мере появления z удовлетворяющего не (y ≤ f z).

LaTeX

$$$\\operatorname{Tendsto}(f,l,\\,\\mathcal{N}(x)) \\iff \\forall y, ¬(y \\le x) \\rightarrow \\forall^{\\infty} z \\in l, ¬(y \\le f(z))$$$

Lean4

theorem tendsto_nhds_iff_not_le {β : Type*} {f : β → α} {l : Filter β} {x : α} :
    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, ¬y ≤ x → ∀ᶠ z in l, ¬y ≤ f z := by
  simp [topology_eq_lowerTopology, tendsto_nhds_generateFrom_iff, Filter.Eventually, Ici, compl_setOf]

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