prod_rightl — Mathlib

English

Let h be IsBigOWith c l f g'. Then h implies IsBigOWith c l f (x ↦ (g'(x), k'(x))).

Русский

Пусть h = IsBigOWith c l f g'. Тогда из h следует IsBigOWith c l f (x ↦ (g'(x), k'(x))).

LaTeX

$$$(h: IsBigOWith\\ c\\ l\\ f\\ g') \\Rightarrow IsBigOWith\\ c\\ l\\ f\\ (\\lambda x.(g'(x), k'(x)))$$$

Lean4

theorem prod_rightl (h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun x => (g' x, k' x) :=
  (h.trans isBigOWith_fst_prod hc).congr_const (mul_one c)

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