English
Let G be a linearly ordered commutative group. If a ≤ b ≤ c and d is any element of G, then the multiplicative absolute value of b divided by d is bounded above by the maximum of c/d and d/a; i.e., |b/d|_m ≤ max(c/d, d/a).
Русский
Пусть G — упорядоченная коммутативная группа. Если a ≤ b ≤ c и любое d ∈ G, то |b/d|ₘ ≤ max(c/d, d/a).
LaTeX
$$$a \le b \le c \implies |b/d|_m \le \max\left( \frac{c}{d}, \frac{d}{a} \right)$$$
Lean4
@[to_additive]
theorem mabs_div_le_max_div {a b c : G} (hac : a ≤ b) (hcd : b ≤ c) (d : G) : |b / d|ₘ ≤ max (c / d) (d / a) :=
by
rcases le_total d b with h | h
· rw [mabs_of_one_le <| one_le_div'.mpr h]
exact le_max_of_le_left <| div_le_div_right' hcd _
· rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]
exact le_max_of_le_right <| div_le_div_left' hac _
