abv_add

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#IsAbsoluteValue.abv_add

English

abv(x+y) ≤ abv(x) + abv(y).

Русский

abv(x+y) ≤ abv(x) + abv(y).

LaTeX

$$$\\operatorname{abv}(x+y) \\le \\operatorname{abv}(x) + \\operatorname{abv}(y)$$$

Lean4

theorem abv_add (x y) : abv (x + y) ≤ abv x + abv y :=
  abv_add' x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru