min_le_max_of_mul_le_mul — Mathlib

English

Let α be a linearly ordered set with a multiplication that is monotone in each argument (left and right). 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 [MulLeftStrictMono α] [MulRightMono α] (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_le_of_lt h.1.1.le h.2.2

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