mono_ge — Mathlib

English

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

Русский

Пусть l — фильтр на α, а u, v: α → β; если l ограничен снизу по ≥ через u и u ≤ᶠ[l] v, то l ограничен снизу по ≥ через v.

LaTeX

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

Lean4

theorem mono_ge [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (· ≥ ·) l u) (hv : u ≤ᶠ[l] v) :
    IsBoundedUnder (· ≥ ·) l v :=
  IsBoundedUnder.mono_le (β := βᵒᵈ) hu hv

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