mabs_max_le_max_mabs_mabs

Mathlib.Algebra.Order.Group.Abs

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

← MathLib Explorer

English

|max(a,b)|_m ≤ max(|a|_m, |b|_m).

Русский

|max(a,b)|_м ≤ max(|a|_м, |b|_м).

LaTeX

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

Lean4

@[to_additive]
theorem mabs_max_le_max_mabs_mabs : |max a b|ₘ ≤ max |a|ₘ |b|ₘ :=
  (le_total a b).elim (fun h => (congr_arg _ <| max_eq_right h).trans_le <| le_max_right _ _) fun h =>
    (congr_arg _ <| max_eq_left h).trans_le <| le_max_left _ _

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

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

Разделы

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

Аффилиация

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