eventually_mem — Mathlib

English

If f tends to l2 along l1 and s ∈ l2, then eventually f(x) ∈ s for x in l1.

Русский

Если f сходится по l1 к l2 и s ∈ l2, то для большинства x по l1 имеем f(x) ∈ s.

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \Rightarrow \operatorname{Membership}.mem l_2 s \Rightarrow \forall^\infty x \in l_1, f(x) \in s $$$$

Lean4

theorem eventually_mem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β} (hf : Tendsto f l₁ l₂) (h : s ∈ l₂) :
    ∀ᶠ x in l₁, f x ∈ s :=
  hf h

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