linearGrowthInf_add_le' — Mathlib

English

A variant of InfAddLe with the order of the arguments swapped: linearGrowthInf (u+v) ≤ linearGrowthInf u + linearGrowthSup v.

Русский

Вариант InfAddLe с поменянным порядком аргументов: linearGrowthInf (u+v) ≤ linearGrowthInf u + linearGrowthSup v.

LaTeX

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

Lean4

/-- See `linearGrowthInf_add_le` for a version with swapped argument `u` and `v`. -/
theorem linearGrowthInf_add_le' (h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤)
    (h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥) :
    linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v :=
  by
  rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]
  exact linearGrowthInf_add_le h'.symm h.symm

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