mul — Mathlib

English

If for every i in a finite multiset s we have f(i) =Θ_l g(i), then the product over i∈s of f(i) is Θ_l the product over i∈s of g(i).

Русский

Если для каждого индекса i в мультисетe s выполняется f(i) =Θ_l g(i), то произведение по i∈s f(i) эквивалентно Θ_l произведению по i∈s g(i).

LaTeX

$$$ (\forall i \in s, f(i) =Θ[l] g(i)) \Rightarrow (\prod_{i \in s} f(i)) =Θ[l] (\prod_{i \in s} g(i)). $$$

Lean4

theorem mul {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
    (fun x ↦ f₁ x * f₂ x) =Θ[l] fun x ↦ g₁ x * g₂ x :=
  h₁.smul h₂

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