frequently — Mathlib

English

If Tendsto f l1 l2 and f(x) frequently satisfies p, then p holds frequently in l2.

Русский

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

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \Rightarrow \operatorname{Frequently} (\lambda y. p(y)) l_2 $$$$

Lean4

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

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