tendsto_iff_forall_eventually_mem

English

Tendsto f l1 l2 iff for every s in l2, eventually f(x) ∈ s along l1.

Русский

Сходимость f по l1 к l2 эквивалентна тому, что для каждого множества s, принадлежащего l2, выполняется f(x) ∈ s почти наверняка по l1.

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \iff \forall s \in l_2, \forall^\infty x \in l_1, f(x) \in s $$$$

Lean4

theorem tendsto_iff_forall_eventually_mem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ x in l₁, f x ∈ s :=
  Iff.rfl

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