isLittleO_comm — Mathlib

English

Little-o relative to a function g is symmetric in the first argument: if f1 - f2 = o(g), then f2 - f1 = o(g).

Русский

Малый порядок по отношению к функции g симметричен к первому аргументу: если f1 - f2 = o(g), то f2 - f1 = o(g).

LaTeX

$$$(f_1 - f_2) = o_l\\, g \\iff (f_2 - f_1) = o_l\\, g$$$

Lean4

theorem isLittleO_comm : (fun x => f₁ x - f₂ x) =o[l] g ↔ (fun x => f₂ x - f₁ x) =o[l] g :=
  ⟨IsLittleO.symm, IsLittleO.symm⟩

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