isBigO_bot — Mathlib

English

For any constant c and any two functions f and g, the relation IsBigOWith c with the bottom filter holds automatically.

Русский

Для любого постоянного c и любых двух функций f и g отношение IsBigOWith c ⊥ f g выполняется автоматически.

LaTeX

$$$\forall c\in\mathbb{R},\; \forall f,g:\; IsBigOWith c \bot f g$$$

Lean4

@[simp]
theorem isBigO_bot : f =O[⊥] g :=
  (isBigOWith_bot 1 f g).isBigO

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