English
Let f: α → E, g' : α → F', and a family f' : α → E' and g' : α → F'. If f is bounded by g' in the sense of IsBigOWith with constant c ≥ 0, then the pair valued map x ↦ (f'(x), g'(x)) is likewise bounded by f with the same constant c; i.e., f = O_l to the map x ↦ (f'(x), g'(x)).
Русский
Пусть f: α → E, g': α → F', и семейство f': α → E', g': α → F'. Если поведение f ограничено относительно g' в смысле IsBigOWith с константой c ≥ 0, тогда пара-значная отображение x ↦ (f'(x), g'(x)) также ограничено по F относительно f; то есть f = O_l (x ↦ (f'(x), g'(x))).
LaTeX
$$$f =O_l g' \quad \Rightarrow \quad f =O_l \bigl( x \mapsto (f'(x), g'(x)) \bigr)\quad( c\ge 0 )$$$
Lean4
theorem prod_rightr (h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun x => (f' x, g' x) :=
(h.trans isBigOWith_snd_prod hc).congr_const (mul_one c)
