smul — Mathlib

English

If for every i in a finite list L we have f_i =Θ_l g_i, then the product over i∈L of f_i(x) equals Θ_l of the product over i∈L of g_i(x).

Русский

Если для каждого индекса i в конечном списке L выполняется f_i =Θ_l g_i, то произведение по i∈L f_i(x) эквивалентно Θ_l произведению по i∈L g_i(x).

LaTeX

$$$ \text{If } \forall i \in L: f_i =Θ[l] g_i, \quad \prod_{i \in L} f_i(x) =Θ[l] \prod_{i \in L} g_i(x). $$$

Lean4

theorem smul [NormedSpace 𝕜 E'] [NormedSpace 𝕜' F'] {f₁ : α → 𝕜} {f₂ : α → 𝕜'} {g₁ : α → E'} {g₂ : α → F'}
    (hf : f₁ =Θ[l] f₂) (hg : g₁ =Θ[l] g₂) : (fun x ↦ f₁ x • g₁ x) =Θ[l] fun x ↦ f₂ x • g₂ x :=
  ⟨hf.1.smul hg.1, hf.2.smul hg.2⟩

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