right_isTheta_add'

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.right_isTheta_add'

English

If f1 = o_l f2, then f2 = Θ_l (f2 + f1).

Русский

Если f1 = o_l f2, то f2 = Θ_l (f2 + f1).

LaTeX

$$$\forall f_1,f_2:\; f_1 =o_{\ell} f_2 \implies f_2 =\Theta_{\ell}(f_2+f_1)$$$

Lean4

theorem right_isTheta_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₂ + f₁) :=
  add_comm f₁ f₂ ▸ h.right_isTheta_add

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

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

Разделы

Аффилиация

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