neg

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

← MathLib Explorer

English

If u ~_l v, then -u ~_l -v.

Русский

Если u эквивалентно v по l, то -u эквивалентно -v по l.

LaTeX

$$$ u \\sim_{l} v \\Rightarrow (-u) \\sim_{l} (-v) $$$

Lean4

theorem neg (huv : u ~[l] v) : (fun x ↦ -u x) ~[l] fun x ↦ -v x :=
  by
  rw [IsEquivalent]
  convert huv.isLittleO.neg_left.neg_right
  simp [neg_add_eq_sub]

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

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

Разделы

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

Аффилиация

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