tendsto_atBot — Mathlib

English

Dual statement to Tendsto_atTop: Tendsto m f atBot if and only if for every b, eventually m(a) ≤ b.

Русский

Двойственность к Tendsto_atTop: Tendsto m f atBot тогда и только тогда, когда для всякого b существует множество a с неравенством m(a) ≤ b.

LaTeX

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

Lean4

theorem tendsto_atBot [Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atBot ↔ ∀ b, ∀ᶠ a in f, m a ≤ b :=
  @tendsto_atTop α βᵒᵈ _ m f

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