English
If f: α → β is a measurable-like map, Tendsto f l1 l2 and p, q relate, then frequently maps through f: frequently x with p(x) implies frequently y with q(y).
Русский
Если f: α → β пределится и p, q связаны, то частотность сохраняется сквозь отображение f: если p(x) часто, то q(f(x)) часто.
LaTeX
$$$$ \forall {l_1 l_2} \ (f) \ (c : \operatorname{Tendsto} f l_1 l_2)\ (w : \forall x, p x \to q (f x))\ (h : \exists^\infty x in l_1, p x) \Rightarrow \exists^\infty y in l_2, q y $$$$
Lean4
theorem frequently_map {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop} (f : α → β)
(c : Filter.Tendsto f l₁ l₂) (w : ∀ x, p x → q (f x)) (h : ∃ᶠ x in l₁, p x) : ∃ᶠ y in l₂, q y :=
c.frequently (h.mono w)
