isTheta_const_smul_right — Mathlib

English

A nonzero scalar on the right preserves Theta equivalence of f and g when f =Θ_l g.

Русский

Ненулевой скаляр справа сохраняет Theta-эквивалентность f и g.

LaTeX

$$$ (f =Θ[l] g) \Rightarrow (f =Θ[l] (c·g) ) \Leftrightarrow (f =Θ[l] g) $.$$

Lean4

theorem isTheta_const_smul_right [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun x ↦ c • g' x) ↔ f =Θ[l] g' :=
  and_congr (isBigO_const_smul_right hc) (isBigO_const_smul_left hc)

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