English
If every index i in a finite list L satisfies f_i = o_l g_i and there exists an i with f_i = o_l g_i, then the product over i in L of f_i is o_l the product over i in L of g_i.
Русский
Если для всех i∈L выполнено f_i = o_l g_i и существует i с f_i = o_l g_i, тогда произведение по i∈L f_i = o_l произведения по i∈L g_i.
LaTeX
$$$ (\\forall i \\in L,\\; f i =o[l] g i) \\land (\\Exists i \\in L,\\; f i =o[l] g i) \\Rightarrow (\\lambda x. (L.map (f \\cdot x)).prod) =o[l] (\\lambda x. (L.map (g \\cdot x)).prod) $$$
Lean4
@[simp]
theorem isLittleO_pure {x} : f'' =o[pure x] g'' ↔ f'' x = 0 :=
calc
f'' =o[pure x] g'' ↔ (fun _y : α => f'' x) =o[pure x] fun _ => g'' x := isLittleO_congr rfl rfl
_ ↔ f'' x = 0 := isLittleO_const_const_iff
