English
For functions f: α → E and g: α → F and k: α → G, the pair (f, g) is Big-O of k if and only if f is Big-O of k and g is Big-O of k.
Русский
Для функций f: α → E, g: α → F и k: α → G верна эквивалентность: (f, g) =O_{𝕜;l} k тогда и только тогда, когда f =O_{𝕜;l} k и g =O_{𝕜;l} k.
LaTeX
$$$ (f,g) =O_{𝕜;l} k \;\iff\; (f =O_{𝕜;l} k) \land (g =O_{𝕜;l} k). $$$
Lean4
@[simp]
theorem isBigOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} :
(fun x ↦ (f x, g x)) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k :=
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩