fst — Mathlib

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

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