trans_eventuallyEq

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.trans_eventuallyEq

English

If f ~_l g1 and g1 =ᶠ[l] g2, then f ~_l g2.

Русский

Если f эквивалентно g1 по l, и g1 равно по l в точности g2, то f эквивалентно g2 по l.

LaTeX

$$f ~_l' g_1 \Rightarrow g_1 =^\!{l} g_2 \Rightarrow f ~_l g_2$$

Lean4

@[trans]
theorem trans_eventuallyEq {f g₁ g₂ : α → β} (h : f ~[l] g₁) (h₂ : g₁ =ᶠ[l] g₂) : f ~[l] g₂ :=
  h.trans h₂.isEquivalent

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

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

Разделы

Аффилиация

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