English
If f is monotone and frequently bounded below by l, then the mapped filter F.map f frequently bounds below by f l after the appropriate lattice embedding.
Русский
Если f монотонна и часто ограничена снизу от l, то отображённый фильтр F.map f часто ограничивает снизу через f l в подходящем отображении решётки.
LaTeX
$$$\text{frequently }(\lambda x, \dots)\; F \mapsto \text{Frequently }(\dots)$$$
Lean4
theorem frequently_ge_map_of_frequently_ge {f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) :
∃ᶠ x' in F.map f, f l ≤ x' := by
refine fun ev ↦ freq_ge ?_
simp only [not_le] at ev freq_ge ⊢
filter_upwards [ev] with z hz
by_contra con
exact lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz