sup' — Mathlib

English

If h and h' are two Big-OWith bounds with possibly different constants, their max constant and the join of the two filters give a combined bound.

Русский

Если есть две границы Big-OWith с разными константами, их максимум констант и объединение фильтров дают совокупную границу.

LaTeX

$$$\text{sup}'\left(h,h'\right): IsBigOWith \max(c,c') (l ⊔ l') f g'$$

Lean4

theorem sup' (h : IsBigOWith c l f g') (h' : IsBigOWith c' l' f g') : IsBigOWith (max c c') (l ⊔ l') f g' :=
  IsBigOWith.of_bound <| mem_sup.2 ⟨(h.weaken <| le_max_left c c').bound, (h'.weaken <| le_max_right c c').bound⟩

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