isBigOWith_snd_prod — Mathlib

English

For any f' : α → E' and g' : α → F', and l a filter, the IsBigOWith c l f' (fst of product) holds with c = 1. More precisely, (f' is a bound for its first coordinate) holds: IsBigOWith 1 l f' (x ↦ (fst (f'(x)), snd (f'(x))))

Русский

Для любых f' : α → E' и g' : α → F' и l — фильтр. Тогда IsBigOWith при лямбда-функции, берет первый компонент пары, выполняется с константой 1.

LaTeX

$$$IsBigOWith\\_1\\ l\\ f'\\ (x \\mapsto (f'(x), g'(x)))$$$

Lean4

theorem isBigOWith_snd_prod : IsBigOWith 1 l g' fun x => (f' x, g' x) :=
  isBigOWith_of_le l fun _x => le_max_right _ _

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