isBigO

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.isBigO

English

For any function u, u is asymptotically equivalent to itself along any filter l.

Русский

Для любой функции u она асимптотически эквивалентна самой себе вдоль любого фильтра l.

LaTeX

$$$\text{Refl: } u ~[l] u$$$

Lean4

nonrec theorem isBigO (h : u ~[l] v) : u =O[l] v :=
  (IsBigO.congr_of_sub h.isBigO.symm).mp (isBigO_refl _ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru