mono_le — Mathlib

English

Let l be a filter on α and u, v: α → β with [Preorder β]. If l is bounded under ≤ by u and v ≤ᶠ[l] u, then l is bounded under ≤ by v.

Русский

Пусть l — фильтр на α, а u, v: α → β; если l ограничен сверху по ≤ через u и v асимптотически меньшe/равно по l к u, то l ограничен сверху по ≤ через v.

LaTeX

$$$ hu : IsBoundedUnder (\le) l u \quad hv : v \le^l u \quad\Rightarrow\ IsBoundedUnder (\le) l v $$$

Lean4

theorem mono_le [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (· ≤ ·) l u) (hv : v ≤ᶠ[l] u) :
    IsBoundedUnder (· ≤ ·) l v := by
  apply hu.imp
  exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

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