antisymm

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.antisymm

English

The Theta relation is symmetric with respect to swapping the two functions.

Русский

Отношение Theta симметрично при обмене двух функций.

LaTeX

$$$ f =Θ[l] g \Rightarrow g =Θ[l] f. $$$

Lean4

theorem antisymm (h₁ : f =O[l] g) (h₂ : g =O[l] f) : f =Θ[l] g :=
  ⟨h₁, h₂⟩

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

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

Разделы

Аффилиация

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