symm

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

Symmetry of asymptotic equivalence: if u ~[l] v then v ~[l] u.

Русский

Симметрия асимптотической эквивалентности: если u ~[l] v, то v ~[l] u.

LaTeX

$$u ~[l] v ⇒ v ~[l] u$$

Lean4

@[symm]
theorem symm (h : u ~[l] v) : v ~[l] u :=
  (h.isLittleO.trans_isBigO h.isBigO_symm).symm

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

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

Разделы

Аффилиация

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