isLittleOTVS_pi — Mathlib

English

For a family f_i, if each f_i =O(g), then the combined function f = (f_i) also satisfies f =O of the product g coordinatewise.

Русский

Для семейства функций f_i, если каждая f_i = O(g), тогда объединенная функция f = (f_i) удовлетворяет f = O(g) по координатам.

LaTeX

$$$\forall i,\ f_i =O_{𝕜;l} g \Rightarrow (\lambda x, (f x)_i) =O_{𝕜;l} g.$$$

Lean4

theorem isLittleOTVS_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⟩

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