tendsto_atTop — Mathlib

English

A general characterization: Tendsto m f atTop is equivalent to m(a) being eventually bounded below by every b, i.e., b ≤ m(a) eventually holds for all b.

Русский

Общее описание: Tendsto m f atTop эквивалентно тому, что для всякого b множество элементов a с b ≤ m(a) встречает бесконечно часто.

LaTeX

$$$$ \operatorname{Tendsto} m\ f\ atTop \iff \forall b, \forall^{\infty} a \ in\ f,\ b \le m(a). $$$$

Lean4

theorem tendsto_atTop [Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atTop ↔ ∀ b, ∀ᶠ a in f, b ≤ m a := by
  simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]

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