tendsto_pure — Mathlib

English

For f: α → β and a filter a on α, Tendsto f a (pure b) iff all a eventually map into the singleton {b}.

Русский

Для функции f: α → β и фильтра a на α, Tendsto f a (pure b) эквивалентно тому, что почти все значения f(a) лежат в {b}.

LaTeX

$$$ \\operatorname{Tendsto} f a \\mathrm{pure}(b) \\iff \\forall^\\infty x \\text{ in } a, f(x) = b $$$

Lean4

@[simp]
theorem tendsto_pure {f : α → β} {a : Filter α} {b : β} : Tendsto f a (pure b) ↔ ∀ᶠ x in a, f x = b := by
  simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]

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