min_le_max_of_mul_le_mul — Mathlib

English

If a·b ≤ c·d in a linearly ordered α with left-strict-monotone and right-strict-monotone multiplication, then min{a,b} ≤ max{c,d}.

Русский

Если a·b ≤ c·d в линейно упорядоченном α с двойной строгой монотонностью умножения, то min{a,b} ≤ max{c,d}.

LaTeX

$$$\\forall a,b,c,d \in \alpha:\; a b \le c d \Rightarrow \min\{a,b\} \le \max\{c,d\}$$$

Lean4

@[to_additive]
theorem min_le_max_of_mul_le_mul [MulLeftStrictMono α] [MulRightStrictMono α] (h : a * b ≤ c * d) : min a b ≤ max c d :=
  haveI := mulRightMono_of_mulRightStrictMono α
  Left.min_le_max_of_mul_le_mul h

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