isBigO_const_const — Mathlib

English

If c is a fixed vector and c' ≠ 0, then the relation (f) =O_l(f') with a constant depending on norms: there is a bound with constant ∥c∥/∥c'∥.

Русский

Пусть c, c' фиксированы, c' ≠ 0; тогда существует константа ∥c∥/∥c'∥, при помощи которой f =O_l f' обходится.

LaTeX

$$IsBigO l (fun _x => c) (fun _x => c')$$

Lean4

theorem isBigO_const_const (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) : (fun _x : α => c) =O[l] fun _x => c' :=
  (isBigOWith_const_const c hc' l).isBigO

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