isTheta_rfl

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.isTheta_rfl

English

Symmetry property for LittleOTVS: swapping the two functions preserves the relation.

Русский

Симметрия LittleOTVS: обмен двух функций сохраняет отношение.

LaTeX

$$$ \text{symm} : f =o_{𝕜;l} g \Rightarrow g =o_{𝕜;l} f. $$$

Lean4

theorem isTheta_rfl : f =Θ[l] f :=
  isTheta_refl _ _

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

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

Разделы

Аффилиация

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