tendsto_nhds_top_iff_real — Mathlib

English

A map m: α → EReal tends to ⊤ if and only if for every real x, m eventually exceeds x.

Русский

Функция m: α → EReal стремится к ⊤ тогда и только тогда, когда для каждого вещественного x существует далее m(a) > x.

LaTeX

$$$\\ Tendsto m f (\\mathcal{N}(\\top)) \\iff \\forall x\\in\\mathbb{R},\\ \\forall^* a\\ in\\ f, x < m(a)$$$

Lean4

theorem tendsto_nhds_top_iff_real {α : Type*} {m : α → EReal} {f : Filter α} :
    Tendsto m f (𝓝 ⊤) ↔ ∀ x : ℝ, ∀ᶠ a in f, ↑x < m a :=
  nhds_top_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Ioi]

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