mabs_div_le

Mathlib.Algebra.Order.Group.Abs

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

← MathLib Explorer

English

For a, b, c in G, |a/c|_m ≤ |a/b|_m · |b/c|_m.

Русский

Для a, b, c в G: |a/c|_м ≤ |a/b|_м · |b/c|_м.

LaTeX

$$$\left| \frac{a}{c} \right|_m \le \left| \frac{a}{b} \right|_m \; \left| \frac{b}{c} \right|_m$$

Lean4

@[to_additive]
theorem mabs_div_le (a b c : G) : |a / c|ₘ ≤ |a / b|ₘ * |b / c|ₘ :=
  calc
    |a / c|ₘ = |a / b * (b / c)|ₘ := by rw [div_mul_div_cancel]
    _ ≤ |a / b|ₘ * |b / c|ₘ := mabs_mul_le _ _

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

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

Разделы

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

Аффилиация

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