mabs_div_le_of_le_of_le — Mathlib

English

Let G be a linearly ordered group with lb ≤ a ≤ ub and lb ≤ b ≤ ub. Then the absolute value of a/b is bounded above by ub/lb: |a/b|_m ≤ ub/lb.

Русский

Пусть G — линейно упорядоченная группа, и lb ≤ a ≤ ub, lb ≤ b ≤ ub. Тогда |a/b|ₘ ≤ ub/lb.

LaTeX

$$$|a/b|_m \le \dfrac{ub}{lb}$$$

Lean4

@[to_additive]
theorem mabs_div_le_of_le_of_le {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) :
    |a / b|ₘ ≤ ub / lb :=
  mabs_div_le_iff.2 ⟨div_le_div'' hau hbl, div_le_div'' hbu hal⟩

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