norm_abs_sub_abs

Mathlib.Analysis.Normed.Order.Lattice

URI: https://scilib.ai/kg/mathlib#norm_abs_sub_abs

English

For any a in a normed lattice-ordered group, ∥|a| − |b|∥ ≤ ∥a − b∥.

Русский

Для любых a,b в нормированной упорядоченной группе выполняется ∥|a| − |b|∥ ≤ ∥a − b∥.

LaTeX

$$$\|\,|a| - |b|\,\| \le \|a - b\|$$$

Lean4

theorem norm_abs_sub_abs (a b : α) : ‖|a| - |b|‖ ≤ ‖a - b‖ :=
  solid (abs_abs_sub_abs_le _ _)

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

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

Разделы

Аффилиация

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