isBigO_sub_rev — Mathlib

English

For a continuous linear equivalence e, the map x' ↦ e(x' − x) isBigO of x' − x in the reverse direction, i.e., the identity can be pulled back through e preserving the asymptotics.

Русский

Для непрерывного линейного эквивалента e отображение x' − x переносится обратно через e с сохранением асимптотики.

LaTeX

$$$$ (x' \\mapsto e(x' - x)) =O_{l} (x' \\mapsto x' - x).$$$$

Lean4

theorem isBigO_sub_rev (l : Filter E) (x : E) : (fun x' => x' - x) =O[l] fun x' => e (x' - x) :=
  e.isBigO_comp_rev _ _

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