isBigO_iff_isBigOWith — Mathlib

English

The Big-O relation is equivalent to the existence of a positive constant c such that f is bounded by c times g along l.

Русский

Отношение Big-O эквивалентно существованию положительной константы c, такой что f≤c g вдоль l.

LaTeX

$$$ f =O[l] g \iff \exists c > 0, IsBigOWith c l f g$$$

Lean4

/-- Definition of `IsBigO` in terms of `IsBigOWith`. We record it in a lemma as `IsBigO` is
irreducible. -/
theorem isBigO_iff_isBigOWith : f =O[l] g ↔ ∃ c : ℝ, IsBigOWith c l f g := by rw [IsBigO_def]

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