IsEquivalent — Mathlib

English

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

Русский

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

LaTeX

$$$u ~[l] v \;\land\; u =^l w \Rightarrow w ~[l] v$$$

Lean4

/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l`
  (denoted as `u ~[l] v` in the `Asymptotics` namespace)
  when `u x - v x = o(v x)` as `x` converges along `l`. -/
def IsEquivalent (l : Filter α) (u v : α → β) :=
  (u - v) =o[l] v

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