frequently_ge_map_of_frequently_ge

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

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