addVal_add — Mathlib

English

The valuation of a sum is at least the minimum of the valuations: addVal(a + b) ≥ min(addVal(a), addVal(b)).

Русский

Оценка суммы не меньше минимума оценок сомножителей: addVal(a + b) ≥ min(addVal(a), addVal(b)).

LaTeX

$$$\min\big(\mathrm{addVal}(a), \mathrm{addVal}(b)\big) \le \mathrm{addVal}(a + b)$$$

Lean4

theorem addVal_add {a b : R} : min (addVal R a) (addVal R b) ≤ addVal R (a + b) :=
  (addVal R).map_add _ _

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