BoundedAtFilter — Mathlib

English

A function f is bounded along l if f = O_l(1).

Русский

Функция f ограничена вдоль фильтра l тогда, когда f = O_l(1).

LaTeX

$$$\\mathrm{BoundedAtFilter}(l,f) \\iff \\mathrm{IsBigO}(l,f, (1 : \\alpha \\to \\mathbb{R}))$$$

Lean4

/-- If `l` is a filter on `α`, then a function `f: α → β` is `BoundedAtFilter l`
if `f =O[l] 1`. -/
def BoundedAtFilter [Norm β] (l : Filter α) (f : α → β) : Prop :=
  Asymptotics.IsBigO l f (1 : α → ℝ)

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