English
If a function f from α to E×F is Big-O of a function g with respect to a field 𝕜 and a filter l, then the first coordinate of f is also Big-O of g with respect to 𝕜 and l.
Русский
Пусть f : α → E × F и g : α → G. Если f =O_{𝕜; l} g, то первый компонент f(x) является O_{𝕜; l} g.
LaTeX
$$$\displaystyle \text{If } f: \alpha \to E \times F \text{ and } g: \alpha \to G ext{ with } f =O_{𝕜;l} g, \text{ then } (x \mapsto (f(x))_1) =O_{𝕜;l} g.$$$
Lean4
protected theorem fst {f : α → E × F} {g : α → G} (h : f =O[𝕜; l] g) : (f · |>.fst) =O[𝕜; l] g :=
ContinuousLinearMap.fst 𝕜 E F |>.isBigOTVS_comp |>.trans h