le_expGrowthSup_mul' — Mathlib

English

For sequences u, v: ℕ → ℝ≥0∞, the same bound as above with swapped arguments holds: expGrowthInf(u) + expGrowthSup(v) ≤ expGrowthSup(u·v).

Русский

Для последовательностей u, v: ℕ → ℝ≥0∞ выполняется неравенство с перестановкой аргументов: expGrowthInf(u) + expGrowthSup(v) ≤ expGrowthSup(u·v).

LaTeX

$$$\expGrowthInf(u) + \expGrowthSup(v) \le \expGrowthSup(u \cdot v)$$$

Lean4

/-- See `le_expGrowthSup_mul` for a version with swapped argument `u` and `v`. -/
theorem le_expGrowthSup_mul' : expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v) :=
  by
  rw [mul_comm, add_comm]
  exact le_expGrowthSup_mul

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