frequently_ge_map_of_frequently_le

English

If f is antitone, frequent lower bounds carry over to the mapped filter under the reversed lattice.

Русский

Если f антито́нна, часто встречающиеся нижние границы переносятся на отображённый фильтр в обратном порядке.

LaTeX

$$Antitone.frequently_ge_map_of_frequently_le$$

Lean4

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

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