IsBounded — Mathlib

English

IsBounded r f means there exists b such that eventually r x b holds for x in f.

Русский

IsBounded r f означает, что существует b, такое что в пределе относительно f выполняется r x b.

LaTeX

$$$\mathrm{IsBounded}\;r\;f \;\equiv\; \exists b, \forall^\mathrm{f} x \in f,\; r(x,b).$$$

Lean4

/-- `f.IsBounded r`: the filter `f` is eventually bounded w.r.t. the relation `r`,
i.e. eventually, it is bounded by some uniform bound.
`r` will be usually instantiated with `(· ≤ ·)` or `(· ≥ ·)`. -/
def IsBounded (r : α → α → Prop) (f : Filter α) :=
  ∃ b, ∀ᶠ x in f, r x b

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