tendsto_pure_left — Mathlib

English

For f: α → β, a ∈ α, and l a filter on β, Tendsto f (pure a) l ⇔ ∀ s ∈ l, f a ∈ s.

Русский

Для функции f: α → β, a ∈ α и фильтра l на β, Tendsto f (pure a) l эквивалентно ∀ s ∈ l, f a ∈ s.

LaTeX

$$$ \\operatorname{Tendsto} f (\\mathrm{pure}(a)) l \\iff \\forall s \\in l, f(a) \\in s $$$

Lean4

theorem tendsto_pure_left {f : α → β} {a : α} {l : Filter β} : Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s :=
  Iff.rfl

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