tendsto_iff_eventually — Mathlib

English

Tendsto f l1 l2 is equivalent to: for every property p, if p holds eventually on l2, then p(f(x)) holds eventually on l1.

Русский

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

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \iff \forall p:\beta\to\text{Prop}, (\forall^\infty y \in l_2, p(y)) \to (\forall^\infty x \in l_1, p(f(x))) $$$$

Lean4

theorem tendsto_iff_eventually {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ y in l₂, p y) → ∀ᶠ x in l₁, p (f x) :=
  Iff.rfl

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