le_linearGrowthSup_add' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See `le_linearGrowthSup_add` for a version with swapped argument `u` and `v`. -/
theorem le_linearGrowthSup_add' : linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v) :=
  by
  rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]
  exact le_linearGrowthSup_add

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