isEquivalent_zero_iff_eventually_zero

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.isEquivalent_zero_iff_eventually_zero

English

u ~[l] 0 iff u converges to 0 along l, i.e., u =ᶠ[l] 0.

Русский

u эквивалентно нулю вдоль l тогда и только тогда u стремится к 0 вдоль l, т.е. u =ᶠ[l] 0.

LaTeX

$$$u ~[l] 0 \iff u =^l 0$$$

Lean4

theorem isEquivalent_zero_iff_eventually_zero : u ~[l] 0 ↔ u =ᶠ[l] 0 :=
  by
  rw [IsEquivalent, sub_zero]
  exact isLittleO_zero_right_iff

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

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

Разделы

Аффилиация

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