isTheta_symm

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

If u ~[l] v, then v =Θ[l] u.

Русский

Если u ~[l] v, то v =Θ[l] u.

LaTeX

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

Lean4

theorem isTheta_symm (h : u ~[l] v) : v =Θ[l] u :=
  ⟨h.isBigO_symm, h.isBigO⟩

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

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

Разделы

Аффилиация

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