isBigO_const — Mathlib

English

Let l be a filter on α. If a function f: α → E is bounded along l (i.e., ‖f(x)‖ is bounded for x in l) and c ≠ 0, then f = O_l (λ x, c).

Русский

Пусть l — фильтр на α. Если функция f: α → E ограничена вдоль l (‖f(x)‖ ограничена вдоль l) и c ≠ 0, то f = O_l (λ x, c).

LaTeX

$$$ (\|f(x)\|) \text{ ограничено вдоль } l \quad \land \ c \neq 0 \ \Longrightarrow\ f =O[l](\lambda x. c). $$$

Lean4

theorem _root_.Filter.IsBoundedUnder.isBigO_const (h : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) {c : F''} (hc : c ≠ 0) :
    f =O[l] fun _x => c :=
  (h.isBigO_one ℝ).trans (isBigO_const_const _ hc _)

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