English
If for all i in a finite set s, f i =O_l g i and there exists i in s with f i = o_l g i, then the finite product over s of f i is o_l the finite product over s of g i.
Русский
Если для всех i в конечном множестве s справедливо f i = O_l 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) \\land (\\exists i \\in s,\\; f i =o[l] g i) \\Rightarrow (∏ i ∈ s, f i \\cdot) =o[l] (∏ i ∈ s, g i \\cdot) $$$
Lean4
theorem finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
(h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ i ∈ s, f i =o[l] g i) : (∏ i ∈ s, f i ·) =o[l] (∏ i ∈ s, g i ·) :=
.multisetProd h₁ h₂
