isBigO_comm — Mathlib

English

Let l be a filter on α and f1, f2: α → E and g: α → F. Then (f1 − f2) =O_l g if and only if (f2 − f1) =O_l g.

Русский

Пусть l — фильтр на α и f1, f2: α → E, g: α → F. Тогда (f1 − f2) =O_l g тогда же эквивалентно (f2 − f1) =O_l g.

LaTeX

$$$$ (f_1 - f_2) =O_l g \\iff (f_2 - f_1) =O_l g $$$$

Lean4

theorem isBigO_comm : (fun x => f₁ x - f₂ x) =O[l] g ↔ (fun x => f₂ x - f₁ x) =O[l] g :=
  ⟨IsBigO.symm, IsBigO.symm⟩

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