min_mabs_mabs_le_mabs_max

Mathlib.Algebra.Order.Group.Abs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem min_mabs_mabs_le_mabs_max : min |a|ₘ |b|ₘ ≤ |max a b|ₘ :=
  (le_total a b).elim (fun h => (min_le_right _ _).trans_eq <| congr_arg _ (max_eq_right h).symm) fun h =>
    (min_le_left _ _).trans_eq <| congr_arg _ (max_eq_left h).symm

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

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

Разделы

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

Аффилиация

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