isBigOTVS_pi — Mathlib

English

The product-mk left rule expresses that the big-O relation for a pair is equivalent to the conjunction of big-O relations for each component, with simp form.

Русский

Правило prodMk left выражает эквивалентность отношения Big-O для пары через конъюнкцию для каждой компоненты (упрощенно).

LaTeX

$$$ [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {f : α → E} {g : α → F} {k : α → G},\ (f,g) =O_{𝕜;l} k \iff (f =O_{𝕜;l} k) ∧ (g =O_{𝕜;l} k). $$$

Lean4

theorem isBigOTVS_pi {ι : Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
    [∀ i, TopologicalSpace (E i)] [∀ i, ContinuousSMul 𝕜 (E i)] {f : α → ∀ i, E i} :
    f =O[𝕜; l] g ↔ ∀ i, (f · i) =O[𝕜; l] g :=
  ⟨.proj, .pi⟩

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