isBigOWith_neg_left — Mathlib

English

Let α be a type, E a normed group, F' a normed group, and l a filter. Then IsBigOWith c l (−f'(x)) g is equivalent to IsBigOWith c l f'(x) g.

Русский

Пусть α — тип; f' : α → E; g : α → F'; тогда IsBigOWith(c,l, −f', g) эквивалентно IsBigOWith(c,l, f', g).

LaTeX

$$$IsBigOWith(c,l, -f', g) \\iff IsBigOWith(c,l, f', g)$$$

Lean4

@[simp]
theorem isBigOWith_neg_left : IsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g := by
  simp only [IsBigOWith_def, norm_neg]

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