mabs_le_max_mabs_mabs

Mathlib.Algebra.Order.Group.Abs

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

← MathLib Explorer

English

If a ≤ b ≤ c, then |b|_m ≤ max(|a|_m, |c|_m).

Русский

Если a ≤ b ≤ c, то |b|_м ≤ max(|a|_м, |c|_м).

LaTeX

$$$a \le b \le c \implies |b|_m \le \max(|a|_m, |c|_m)$$$

Lean4

@[to_additive]
theorem mabs_le_max_mabs_mabs (hab : a ≤ b) (hbc : b ≤ c) : |b|ₘ ≤ max |a|ₘ |c|ₘ :=
  mabs_le'.2 ⟨by simp [hbc.trans (le_mabs_self c)], by simp [(inv_le_inv_iff.mpr hab).trans (inv_le_mabs a)]⟩

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

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

Разделы

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

Аффилиация

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