IsBoundedUnder — Mathlib

English

IsBoundedUnder r f u means the image of f under u is bounded with respect to r, i.e. (map u f).IsBounded r.

Русский

IsBoundedUnder r f u означает, что образ фильтра f под u ограничен относительно порядка r, то есть (map u f).IsBounded r.

LaTeX

$$$\mathrm{IsBoundedUnder}\;r\;f\;u \;\equiv\; (\mathrm{map}\;u\;f).\mathrm{IsBounded}\;r.$$$

Lean4

/-- `f.IsBoundedUnder (≺) u`: the image of the filter `f` under `u` is eventually bounded w.r.t.
the relation `≺`, i.e. eventually, it is bounded by some uniform bound. -/
def IsBoundedUnder (r : α → α → Prop) (f : Filter β) (u : β → α) :=
  (map u f).IsBounded r

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