tendsto_nhds_bot_iff_real — Mathlib

English

A map m: α → EReal tends to ⊥ if and only if for every real x, m(a) < x holds eventually along f.

Русский

Функция m: α → EReal стремится к ⊥ тогда и только тогда, когда для каждого вещественного x верно, что m(a) < x выполнено почти всюду вдоль f.

LaTeX

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

Lean4

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

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