tendsto_nhds_iff_not_le — Mathlib

English

In the upper topology, a function f: β → α is continuous with respect to l if and only if for every y, whenever x is not below y, f(z) is eventually not below y; i.e., for all y with x ≰ y, eventually f(z) ≰ y.

Русский

В верхней топологии функция f: β → α непрерывна на фильтре l тогда, когда для каждого y, при котором x не ниже y, выполняется, что для аргументов z из l f(z) в итоге не ниже y; то есть f(z) ≰ y для большинства z.

LaTeX

$$$\text{Filter.Tendsto } f\, l\ (\mathcal{N} x) \iff \forall y, \neg (x \le y) \rightarrow \forall^{\infty} z \in l, \neg (f(z) \le y)$$$

Lean4

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

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