isBigOTVS_prodMk_left — Mathlib

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⟩

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