isTheta_const_mul_right — Mathlib

English

If c is a nonzero scalar in the base field and f: α → E, g: α → 𝕜 with E a normed space, then f =Θ_l(c g) if and only if f =Θ_l g.

Русский

Если c — ненулевой скаляр поля, а f: α → E, g: α → 𝕜, где E — нормированное пространство, то f =Θ_l(c g) тогда и только тогда, когда f =Θ_l g.

LaTeX

$$$\forall \alpha\, (f : \alpha \to E) \ (g : \alpha \to 𝕜)\ (c : 𝕜),\ c \neq 0:\; f =\Theta_{\ell}(c\,g) \;\Leftrightarrow\; f =\Theta_{\ell} g$$$

Lean4

theorem isTheta_const_mul_right {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun x ↦ c * g x) ↔ f =Θ[l] g := by
  simpa only [← smul_eq_mul] using isTheta_const_smul_right hc

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