frequently_le_map_of_frequently_ge

English

In an opposite order, a frequently ge map translates to a frequently le map in the dual order.

Русский

В противоположном порядке часто ге отображение переходит в часто ле отображение в двойственном порядке.

LaTeX

$$Monotone.frequently_ge_map_of_frequently_ge$$

Lean4

theorem frequently_le_map_of_frequently_ge {f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ x in F, l ≤ x) :
    ∃ᶠ y in F.map f, y ≤ f l :=
  Monotone.frequently_ge_map_of_frequently_ge (S := Sᵒᵈ) f_decr frbdd

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