tendsto_principal — Mathlib

English

For any function f, filter l, and set s, Tendsto f l (principal s) iff f takes values in s eventually along l.

Русский

Для произвольной функции f, фильтра l и множества s, Tendsto f l (principal s) эквивалентно тому, что значения f лежат в s почти всегда по l.

LaTeX

$$$ \\operatorname{Tendsto} f l \\mathcal{P}(s) \\iff \\forall^\\infty a \\text{ in } l,\\ f(a) \\in s $$$

Lean4

@[simp]
theorem tendsto_principal {f : α → β} {l : Filter α} {s : Set β} : Tendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s := by
  simp only [Tendsto, le_principal_iff, mem_map', Filter.Eventually]

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