min_le_max_of_mul_le_mul — Mathlib

English

Let α be a linearly ordered set with left-monotone multiplication and right-strictly monotone multiplication. If a·b ≤ c·d, 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 [MulLeftMono α] [MulRightStrictMono α] (h : a * b ≤ c * d) : min a b ≤ max c d := by
  simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

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