mono — Mathlib

English

Let f ≤ g be filters on β and u: β → α. If g is r-bounded under u, then f is r-bounded under u.

Русский

Пусть f ≤ g — фильтры на β и u: β → α. Если g ограничен снизу или сверху относительно r по u, то и f имеет такую же ограниченность.

LaTeX

$$$ f \le g \Rightarrow (g.IsBoundedUnder r u) \Rightarrow (f.IsBoundedUnder r u) $$$

Lean4

theorem mono {f g : Filter β} {u : β → α} (h : f ≤ g) : g.IsBoundedUnder r u → f.IsBoundedUnder r u := fun hg =>
  IsBounded.mono (map_mono h) hg

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