English
Let R be a linearly ordered ring with nonnegative scalars. For all b,c in R, we have max(a b, d c) ≤ max(a,c) · max(d,b) whenever a ≥ 0 and d ≥ 0.
Русский
Пусть R — упорядоченное кольцо; для любых b,c ∈ R выполняется max(a b, d c) ≤ max(a,c)·max(d,b), если a ≥ 0 и d ≥ 0.
LaTeX
$$$$\\text{If } a \\ge 0,\\ d \\ge 0,\\text{ then } \\max(a b, d c) \\le \\max(a,c) \\cdot \\max(d,b) \\text{ for all } b,c.$$$$
Lean4
theorem max_mul_mul_le_max_mul_max [PosMulMono R] [MulPosMono R] (b c : R) (ha : 0 ≤ a) (hd : 0 ≤ d) :
max (a * b) (d * c) ≤ max a c * max d b :=
have ba : b * a ≤ max d b * max c a :=
mul_le_mul (le_max_right d b) (le_max_right c a) ha (le_trans hd (le_max_left d b))
have cd : c * d ≤ max a c * max b d :=
mul_le_mul (le_max_right a c) (le_max_right b d) hd (le_trans ha (le_max_left a c))
max_le (by simpa [mul_comm, max_comm] using ba) (by simpa [mul_comm, max_comm] using cd)
