abs_abv_sub_le_abv_sub

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.abs_abv_sub_le_abv_sub

← MathLib Explorer

English

For all a,b ∈ R, |abv(a) − abv(b)| ≤ abv(a − b).

Русский

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

LaTeX

$$$\\left|\\operatorname{abv}(a) - \\operatorname{abv}(b)\\right| \\le \\operatorname{abv}(a-b)$$$

Lean4

@[bound]
theorem abs_abv_sub_le_abv_sub (a b : R) : abs (abv a - abv b) ≤ abv (a - b) :=
  abs_sub_le_iff.2 ⟨abv.le_sub _ _, by rw [abv.map_sub]; apply abv.le_sub⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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