isEquivalent — Mathlib

English

If two functions u and v are eventually equal with respect to a filter l, then they are asymptotically equivalent with respect to l.

Русский

Если две функции u и v совпадают вплоть до элементов множества из фильтра l, то они асимптотически эквивалентны по отношению к l.

LaTeX

$$$u =^\!{l} v \Rightarrow u \sim_l v$$$

Lean4

theorem isEquivalent {u v : α → β} (h : u =ᶠ[l] v) : u ~[l] v :=
  IsEquivalent.congr_right (isLittleO_refl_left _ _) h

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