abv_sub_le

Mathlib.Algebra.Order.AbsoluteValue.Basic

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

English

For a,b,c ∈ R with IsAbsoluteValue abv, abv(a) − abv(c) ≤ abv(a − b) + abv(b − c).

Русский

Для любых a,b,c ∈ R с abv, выполняется abv(a) − abv(c) ≤ abv(a − b) + abv(b − c).

LaTeX

$$$abv(a) - abv(c) \le abv(a - b) + abv(b - c)$$$

Lean4

theorem abv_sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c) := by
  simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

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

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

Разделы

Аффилиация

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