frequently_le_map_of_frequently_le

English

If f is monotone and frequently bounded below by l, then the frequently bounded below by f l holds for the mapped filter F.map f.

Русский

Если f монотонна и часто имеет нижнюю границу l, то для отображённого фильтра F.map f выполняется частая нижняя граница f l.

LaTeX

$$Monotone.frequently_ge_map_of_frequently_ge$$

Lean4

theorem frequently_le_map_of_frequently_le {f : R → S} (f_incr : Monotone f) {u : R} (freq_le : ∃ᶠ x in F, x ≤ u) :
    ∃ᶠ y in F.map f, y ≤ f u := by
  refine fun ev ↦ freq_le ?_
  simp only [not_le] at ev freq_le ⊢
  filter_upwards [ev] with z hz
  by_contra con
  apply lt_irrefl (f u) <| lt_of_lt_of_le hz <| f_incr (not_lt.mp con)

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