le_expGrowthInf_add — Mathlib

English

For sequences u, v, the infimum of the pointwise sum is at least the sum of infima: expGrowthInf u ⊔ expGrowthInf v ≤ expGrowthInf (u+v).

Русский

Для последовательностей u, v верно: infimum ростa u и v сумм равны с суммой infima: expGrowthInf u ⊔ expGrowthInf v ≤ expGrowthInf(u+v).

LaTeX

$$$\expGrowthInf(u) \sqcup \expGrowthInf(v) \le \expGrowthInf(u+v)$$$

Lean4

theorem le_expGrowthInf_add : expGrowthInf u ⊔ expGrowthInf v ≤ expGrowthInf (u + v) :=
  sup_le (expGrowthInf_monotone le_self_add) (expGrowthInf_monotone le_add_self)

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