snd — Mathlib

English

If a function f: α → E×F is Big-O of g, then the second coordinate of f is Big-O of g as well.

Русский

Пусть f : α → E × F и g : α → G. Если f =O_{𝕜;l} g, то второй компонент f(x)^2 является O_{𝕜;l} g.

LaTeX

$$$\displaystyle f =O_{𝕜;l} g \Longrightarrow (x \mapsto (f(x))_2) =O_{𝕜;l} g.$$$

Lean4

protected theorem snd {f : α → E × F} {g : α → G} (h : f =O[𝕜; l] g) : (f · |>.snd) =O[𝕜; l] g :=
  ContinuousLinearMap.snd 𝕜 E F |>.isBigOTVS_comp |>.trans h

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