isBigO_congr_left

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.isBigO_congr_left

English

If f' =Θ_l g' then IsLittleO relation with respect to k is equivalent for f' and g'.

Русский

Если f' =Θ_l g', то отношение little-o относительно k одинаково для f' и g'.

LaTeX

$$$f' =Θ_l g' \\Rightarrow (f' =o_l k \\iff g' =o_l k)$$$

Lean4

theorem isBigO_congr_left (h : f' =Θ[l] g') : f' =O[l] k ↔ g' =O[l] k :=
  ⟨h.symm.trans_isBigO, h.trans_isBigO⟩

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

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

Разделы

Аффилиация

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