proj — Mathlib

English

Projecting a function f: α → ∏ i E_i onto the i-th coordinate preserves the little-o relation with g.

Русский

Проекция функции f: α → ∏ i E_i на i-ю координату сохраняет отношение 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_isLittleOTVS h

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