eventually_mul_div_cancel

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If f^n = o_l g^n with n ≠ 0, then f = o_l g.

Русский

Если f^n = o_l g^n при n ≠ 0, тогда f = o_l g.

LaTeX

$${f^n = o_l g^n} ∧ n ≠ 0 ⇒ f = o_l g.$$

Lean4

/-- If `u = o(v)` along `l`, then `(u / v) * v = u` eventually at `l`. -/
theorem eventually_mul_div_cancel (h : u =o[l] v) : u / v * v =ᶠ[l] u :=
  (h.forall_isBigOWith zero_lt_one).eventually_mul_div_cancel

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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