finsetProd — Mathlib

English

If for every i in a finite set s we have f i =O_l g i, then the product over i in s of f i is O_l the product over i in s of g i.

Русский

Если для каждого элемента i в конечном множестве s выполнено f(i) =O_l(g(i)), тогда произведение по i∈s f(i) имеет порядок O_l произведения по i∈s g(i).

LaTeX

$$$ (\\forall i \\in s,\\; f i =O[l] g i) \\Rightarrow (\\prod i \\in s, f i \\cdot) =O[l] (\\prod i \\in s, g i \\cdot) $$$

Lean4

theorem finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
    (hf : ∀ i ∈ s, f i =O[l] g i) : (∏ i ∈ s, f i ·) =O[l] (∏ i ∈ s, g i ·) :=
  .multisetProd hf

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