proj — Mathlib

English

Projecting a function f: α → E×F onto the i-th coordinate preserves the Big-O relation with g.

Русский

Проекция функции f: α → E×F на i-ю координату сохраняет отношение Big-O с g.

LaTeX

$$$\text{If } f =O_{𝕜;l} g, \text{ then } (f \cdot i) =O_{𝕜;l} g.$$$

Lean4

theorem proj {ι : Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
    {f : α → ∀ i, E i} (h : f =O[𝕜; l] g) (i : ι) : (f · i) =O[𝕜; l] g :=
  ContinuousLinearMap.proj i |>.isBigOTVS_fun_comp |>.trans h

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