isLittleO_congr_right

Mathlib.Analysis.Asymptotics.Theta

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

English

If f' =Θ_l g' and g' ≡_l k' then f' =Θ_l k'.

Русский

Если f' =Θ_l g' и g' эквивалентны k' по l, тогда f' =Θ_l k'.

LaTeX

$$$f' =Θ_l g' \\land g' =ᶠ_l k' \\Rightarrow f' =Θ_l k'$$$

Lean4

theorem isLittleO_congr_right (h : g' =Θ[l] k') : f =o[l] g' ↔ f =o[l] k' :=
  ⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩

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

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

Разделы

Аффилиация

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