isBigO_norm_right — Mathlib

English

The Big-OWith bound with the absolute value of the right-hand side is equivalent to the bound with the right-hand side itself.

Русский

Граница Big-OWith с модулем справа равна границе с самим правым членом.

LaTeX

$$$\bigl(IsBigOWith c l f (|u|)\bigr) \iff \bigl(IsBigOWith c l f u\bigr)$$$

Lean4

@[simp]
theorem isBigO_norm_right : (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g' :=
  by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_right

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