linearGrowthSup_add_le — Mathlib

English

Under appropriate hypotheses, linearGrowthSup (u+v) ≤ linearGrowthSup u + linearGrowthSup v.

Русский

При подходящих предпосылках линейный верхний рост суммы не превышает сумму верхних ростов.

LaTeX

$$$\operatorname{linearGrowthSup}(u+v) \le \operatorname{linearGrowthSup}(u) + \operatorname{linearGrowthSup}(v)$$$

Lean4

theorem linearGrowthSup_add_le (h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤)
    (h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥) :
    linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup v :=
  by
  refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
  rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']

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