trans

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

← MathLib Explorer

English

If u ~[l] v and v ~[l] w, then u ~[l] w.

Русский

Если u эквивалентна v и v эквивалентна w вдоль l, то u эквивалентна w.

LaTeX

$$u ~[l] v ∧ v ~[l] w ⇒ u ~[l] w$$

Lean4

@[trans]
theorem trans {l : Filter α} {u v w : α → β} (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
  (huv.isLittleO.trans_isBigO hvw.isBigO).triangle hvw.isLittleO

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

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

Разделы

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

Аффилиация

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