eventually — Mathlib

English

If f tends to l2 along l1 and ∀ᶠ y in l2, p(y), then ∀ᶠ x in l1, p(f(x)).

Русский

Если f сходится по l1 к l2 и для почти всех y в l2 выполняется p(y), то для почти всех x в l1 выполняется p(f(x)).

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \Rightarrow (\forall^\infty y \in l_2, p(y)) \Rightarrow (\forall^\infty x \in l_1, p(f(x))). $$$$

Lean4

theorem eventually {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Tendsto f l₁ l₂)
    (h : ∀ᶠ y in l₂, p y) : ∀ᶠ x in l₁, p (f x) :=
  hf h

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